New patches: [unrevert anon**20101117195410 Ignore-this: 7c98911eb8d610618e8380d74b7824c5 ] hunk ./Logic.cabal 39 Build-Depends: base, containers, fgl, happstack-data, happstack-state, incremental-sat-solver, mtl, syb-with-class, text, PropLogic, pretty, syb -Executable tests - Main-Is: Test/Test.hs - Build-Depends: - HUnit - Context: [Temporarily disable the tests that don't compile under ghc7 David Fox **20101116213313 Ignore-this: 4e893486da4be4656e2628ce54b9366a ] [Changes to compile with ghc 7, hopefully backwards compatible David Fox **20101116174245 Ignore-this: cd05ab49c4179949360317d0d5659fac ] [Remove debian dependencies on tptp also David Fox **20101102195311 Ignore-this: 89e6ea0846f4dbcf38a95e5d5505e5a6 ] [Version 0.25 - disable Logic-TPTP instance David Fox **20101030173607 Ignore-this: 28306e6c8cae5876802430b02f524553 ] [0.24 - add a missing paren in the show function David Fox **20101021041746 Ignore-this: b5a51114bde9c0c5c4edd0c0efea65a0 ] [Version 0.23 - add a "one" method to class Variable David Fox **20101006193056 Ignore-this: b2afa1f5dcf8e309d3e20b9b026c35f7 ] [Version 0.22 David Fox **20100904172546 Ignore-this: 5db10a311357c88347eaf6f687c5744d ] [Require Pretty instances for all atomic types so we can always pretty print formulas David Fox **20100904171418 Ignore-this: ddad8d7d9277b8a0569f22b67cc65fa8 ] [Replace the pApp method of the FirstOrderFormula with fixed arity versions: pApp0, pApp1, etc David Fox **20100904171246 Ignore-this: d2eabc3d0eec4df60f7d797e388b989e ] [Add withUnivQuants David Fox **20100903201106 Ignore-this: 7e2df8340ee102f1fba324a6718d7a20 ] [Development in Harrison modules David Fox **20100903201052 Ignore-this: 150a9f8397730aa4fc1bae92bbcd211a ] [Add an Arity class and make it a superclass for all predicates David Fox **20100903200345 Ignore-this: 8b5d011e744adf918615802718dfe935 ] [Use a Variable class instead of Enum for generating new variable names David Fox **20100903195440 Ignore-this: 46b0d8c3acb507361a26f63870f53ddd ] [Fix some name space issues David Fox **20100830230719 Ignore-this: e27f6d2e82916c6f8d54852b9957a703 ] [Version 0.21.2 - add cartesianProduct, implement purednf and give purecnf in terms of purednf David Fox **20100830225656 Ignore-this: 97ff719b00be176d3b81a8f2ff02fc38 ] [Fix the conversion from FirstOrderFormula to Literal where zipN was throwing an error instead of returning Nothing, remove two tabs David Fox **20100830224038 Ignore-this: 5ae697f3cffd61fef884d87e3c5430d5 ] [Add debian dependencies on sat-solver packges David Fox **20100830000342 Ignore-this: c5139afd51de41c8679f69684aaca3cf ] [Logic 0.21 David Fox **20100829223241 Ignore-this: c4459bb43c8d971290972582d7859f3b ] [Remove some unnecessary functional dependencies David Fox **20100829173907 Ignore-this: 2fa42c52cc2ef7e85a66e146d11985f9 ] [Use sets instead of lists for SetOfSupport type in Logic.Resolution David Fox **20100829173246 Ignore-this: 57b0bffcf5b2176b6bf09524a7ceb785 ] [Add some Ord instances so we can put Implicative formulas in sets David Fox **20100829171715 Ignore-this: e5660cf771f962231b3f578cb7c2f2b4 ] [Eliminate a left over .~. method from the NormalLogic class, its in Literal now David Fox **20100829171235 Ignore-this: 5275ddda802d5ec60d665c7940ce0039 ] [Make simpcnf convert from FirstOrderLogic to NormalLogic David Fox **20100829164255 Ignore-this: a658d84d4689fd4c2a55867d53f35c90 ] [Make Literal a superclass of Logic, rename its methods invert -> (.~.), inverted -> negated David Fox **20100829144902 Ignore-this: 19cf2d1a4e21f6a1e5c1f6f288f08a2c ] [Add Logic.Normal, change some FirstOrderLogic superclasses to Term David Fox **20100828201044 Ignore-this: 9ff58b5f7512c1f8a9e54a50200fc14f ] [Eliminate more superclasses from the FirstOrderLogic class David Fox **20100828195727 Ignore-this: 70f47d518c97c3c08b1d902b30d2da0 ] [Get rid of some the Show superclasses David Fox **20100828194009 Ignore-this: d5b27f2945003b5acf8c7aa2a6825338 ] [Document the super classes of Term and FirstOrderLogic David Fox **20100828190814 Ignore-this: 1a2292936b92f8309baa241875551417 ] [Fix the superclasses of some Term operations, Remove an unnecessary use of term equality David Fox **20100828170307 Ignore-this: 96d65a3b569acfa9d1bc7c14552eb58a ] [Move the Harrison code back out of Logic.NormalForm David Fox **20100827210235 Ignore-this: f614e0dd108161f5c3341660907b0beb ] [Add some translations of the Harrison OCaml files David Fox **20100827202256 Ignore-this: c554c741ee5226bb99eafe5dcd9595ee ] [Add SatSolver instance David Fox **20100827174035 Ignore-this: 741e1bf0f660161408d99477685f561 ] [Add some functions to Logic.Set - mapM, ssMapM, toSS, fromSS David Fox **20100827171533 Ignore-this: 5a9e50b3719e7c386c7c43efda492f61 ] [Version 0.20 - reduce number of arguments to foldF to three David Fox **20100824215016 Ignore-this: 940f690f7b3a7f912f4cc478a508e3c3 ] [Eliminate the negation argument from foldF and zipF, create a Combine type to describe all formula combinators David Fox **20100823231812 Ignore-this: d850d6934ec8aa923f2063e4c39473e4 ] [Eliminate one of the arguments of foldf, infix predicates are now handled by the same function as prefix David Fox **20100823025044 Ignore-this: 57bf4e438169460cd4341bf34f47bce5 ] [Fix a bug in showForm - lhs was not being parenthesized, rhs was David Fox **20100822191440 Ignore-this: 8830fcd0e02228ee8df6bfd4ade37b9d ] [Merge Test.New into Test.Types, get rid of some tests that don't make sense David Fox **20100822145433 Ignore-this: 6ec317089f61455a0021f678f552a41e ] [The Harrison functions have all moved into Logic.NormalForm David Fox **20100822130656 Ignore-this: 7fbc8db768890e026b74150814d2978d ] [We don't need a monad to compute prenex normal form David Fox **20100822130502 Ignore-this: 70a52db6e7a009c5f270481bac188487 ] [Add new modules to export list David Fox **20100821211215 Ignore-this: 1349c53926193471c63ebf162206da17 ] [Update test cases David Fox **20100821173338 Ignore-this: c4116b3c3a8ae847647b1b3ac9f28c4e ] [Remove a comment that bothers haddock David Fox **20100821173314 Ignore-this: e7ccc26b8664bcefab9aa9d845ab88d4 ] [Move Harrison code into NormalForm David Fox **20100821173146 Ignore-this: af3abd1966e57b25e5bb651d5df3ec35 ] [Update test cases David Fox **20100821164507 Ignore-this: a5cd4d679d2140c71194a21588bc64a1 ] [Changelog entry for 0.19 David Fox **20100821134059 Ignore-this: 49989bf4ac092cd17b326f817721b0a0 ] [Add Logic.Set, a slightly augmented Data.Set module David Fox **20100821134012 Ignore-this: 23f4d9c2342bb3a10784d1ac9e57e9f8 ] [Update some superclasses and function names in Logic.Satisfiable David Fox **20100821133914 Ignore-this: 174b7aba618e78415259732219c14219 ] [Replace routines in Logic.NormalForm with those in Logic.Harrison David Fox **20100821133543 Ignore-this: c7768b772d756e110664900331874640 ] [Add makeINF', which is like makeINF but takes list arguments instead of sets David Fox **20100821133210 Ignore-this: 534395b34223934c60bed10b176332f3 ] [Rename negate -> invert, negated -> inverted to avoid conflict in Prelude David Fox **20100821133055 Ignore-this: fcfd062f5d1d3fd1c42bf3c7d5194209 ] [Finish Harrison implementation of nnf, pnf, skolemize, cnf David Fox **20100821131921 Ignore-this: aa1084b90821ec401beda860863d7036 ] [Use the NormalT monad to generate skolem variables in Logic.Harrison, fix some bugs David Fox **20100819203308 Ignore-this: 6c319e612b607b14a3f5402425c12d32 ] [Add Logic.Harrison, clean up some show issues, add multi-variable versions of the quantifier functions David Fox **20100819174103 Ignore-this: c0e488a0b3c60c10f44c9fce86dd917a ] [Use a single variable instead of a variable list in foldF, quant, for_all, and exists, it simplifies the code David Fox **20100819123200 Ignore-this: 2f0ed395fad99db028ea5d6cff54df58 ] [Version 0.19 David Fox **20100817215553 Ignore-this: 9a95c1cd53d906e18379709dfa90465c ] [Add Test.TPTP David Fox **20100817215837 Ignore-this: 6ea7966320f92cce6be70e87445eb6df ] [Emergency check-in David Fox **20100817212745 Ignore-this: db7b0c5369c38793157b54117615800c ] [Fix a place where we used .|. instead of .&. to implement conj David Fox **20100817152012 Ignore-this: b2cc89caa30715065aaf6d59adf426e6 ] [Update test cases David Fox **20100816202647 Ignore-this: 58d97046a2afae21f9acb695a8de4d7 ] [Update the TPTP instance David Fox **20100816202359 Ignore-this: 669f20792bd129feed76ed2bc45644de ] [Add and export a prettyTerm function David Fox **20100816202322 Ignore-this: 9af82af2cfc8b18b91f9095ffad46332 ] [Rename monad SkolemT to NormalT and merge VariableT into it David Fox **20100816171334 Ignore-this: 6ad3a03187c082a0dbfc3d1c41fadebc ] [Give quantified variables unique names before doing prenex normal form David Fox **20100816164504 Ignore-this: 4b00753fae6b9d9fab808afb4aa9041b ] [Merge Logic.Chiou.* modules into Logic.Instances.Chiou David Fox **20100816002815 Ignore-this: 7268443c72aa023ce2879e0a9c06201 ] [Use Native instance for tests, make test data more polymorphic, make test output more polymorphic David Fox **20100816001611 Ignore-this: 859403eab80e536db0288ff46994e4f2 ] [Rename Logic.Instances.Parameterized -> Logic.Instances.Native David Fox **20100815182415 Ignore-this: cedabd89ae95878f734e4519a4d97761 ] [Use showForm to implement Chiou Show instance, polymorphic Knowledgebase module David Fox **20100815181255 Ignore-this: 87f26708bc3047b4eb15bf399103f0ee ] [Rename Term -> CTerm in Logic.Chiou.FirstOrderLoigc David Fox **20100815164732 Ignore-this: ddf5b8bf80c9d646f80ad894840ad70e ] [Use a Map instead of an alist for the Subst type David Fox **20100815162802 Ignore-this: fe52316f3b1c4e4aed715f139fd6589b ] [Use sets instead of lists in the INF class David Fox **20100815150914 Ignore-this: d9732ccdace1010caa63e159deeb7c32 ] [Rename Clausal to ClauseNormal David Fox **20100815031735 Ignore-this: b733571fc7427bba9698b3956c306661 ] [Restore missing signatures David Fox **20100815030717 Ignore-this: cb3670da60a09acd12abcef10486bef1 ] [Get rid of unnecessary superclasses, move them into instances where possible David Fox **20100815013408 Ignore-this: cfc26d525ce3d584e1858d023c562933 ] [Make the parameters of ProverT and ProverT' more general David Fox **20100814214803 Ignore-this: c44a40c8ef34c2fdfa57730ba7d3fa9b ] [Make Resolution polymorphic David Fox **20100814214240 Ignore-this: 15db1d395cb15a7c0fa7db4d3b0ef408 ] [Fix a bug in animalKB, test case updates, pretty printing David Fox **20100814172530 Ignore-this: 31601b29a29e531fede13df94f2bc85e ] [Put in a new skolemize which propertly maintains LogicState, but intentionally broken (as noted) so our test cases still work David Fox **20100814154033 Ignore-this: 2516328e8b0cc15aba97304b72c46332 ] [Create a monad ProverT' which is a combination of ProverT and SkolemT David Fox **20100814152857 Ignore-this: e65e6fca66effc6dea25ef0713798ea4 ] [Add zip methods to FirstOrderLogic and Term David Fox **20100814144051 Ignore-this: 16f9e3245c0e14d139800fe7f20de8f3 ] [Split a Term class out of the FirstOrderLogic class David Fox **20100813224043 Ignore-this: 2822944e461963636c9cef2443aa058a ] [Simplify the parameters of Subst David Fox **20100813210934 Ignore-this: e621fbf941a1ce37372ec6588fc10906 ] [Get rid of Logic.Chiou.Skolem, Change SentenceCount type back to Int David Fox **20100813182555 Ignore-this: afaa09a94cb0a6666ccb3379345093a2 ] [Move splitSkolem functionality from Logic.Chiou.Skolem to Logic.NormalForm David Fox **20100813180935 Ignore-this: e242afca73ba7948c092d109d6a120e3 ] [Add Data and Typeable instances so we can use gFind et. al. David Fox **20100813175914 Ignore-this: 718f54db83e87b39b171d24a48100e39 ] [Eliminate module names, instead of using a Skolem number to identify which INFs come from a sentence, assign a sentence Id David Fox **20100813171633 Ignore-this: 659b0b27a91e98c579503a0bd680ecbd ] [Clean up and figure out Logic.Chiou.Skolem, add a SkolemSet test to Test.Types David Fox **20100813161635 Ignore-this: 6a4c88c82fc702c8a37a44c5d21406d1 ] [Rename test case SatResult -> SatPropLogic, add test case SatChiou David Fox **20100812170630 Ignore-this: 121dca1da80fd2b7de6e4ff69071785d ] [Rename skolemCount -> skolemOffset in ProverT monad David Fox **20100812170544 Ignore-this: 9890352e7fe7c3ada0e303645630e07a ] [Remove Show superclasses from Chiou prover code David Fox **20100812165235 Ignore-this: 4dac04a9936db80f33d8b5ec91047c09 ] [Do skolemization in a monad (SkolemT) David Fox **20100812131623 Ignore-this: 422132f627687a2e4b3c3a384b463ca4 ] [Remove unused Logic.Conjunctive module David Fox **20100811205802 Ignore-this: 4f938eae532d9bd54221a978070d8468 ] [Replace various implementations of disj and conj with a general one in Logic.FirstOrder. David Fox **20100811205639 Ignore-this: 554c65760558347ee3406d7b43cd682f ] [Change Implicative parameters to inf clause David Fox **20100811204949 Ignore-this: c4e0c992071bc00272d0098dfe694052 ] [Add Logic.Resolution module (incomplete) David Fox **20100811204342 Ignore-this: cdebdfdfbb7e65c29a40a6f953c91f40 ] [clausalNormalForm returns [[formula]] instead of formula David Fox **20100811201428 Ignore-this: 3aec0f1147e6597af5cd6cb3227a20be ] [Add the makeINF method to Implicative, preparing to fix Implicative's type parameters David Fox **20100811191519 Ignore-this: b9ea8f2df1fa65ab008d5e7cf274dc68 ] [Change the return type of neg and pos from a set to a list. David Fox **20100811184344 Ignore-this: c0e43916342e273b9082da89edf907a2 ] [Add tests of the Chiou resolution prover to Test.New David Fox **20100811170643 Ignore-this: 5217818eb1003c590fb0e6e630df9d53 ] [Moving tests into New/Data, skolemNormalForm retains universal quantifiers, add DisjunctiveNormalForm test case David Fox **20100811133718 Ignore-this: 4c2c941eb30fbfa9cb0531c9353e6047 ] [Add the chang example 4.3 tests David Fox **20100811051822 Ignore-this: da7f48029ee4ba12cf0ad3d39939b048 ] [Make V an enum so we can use succ to get new variable names, change variable name sequence David Fox **20100811045803 Ignore-this: fc8406b13fb55f351c59e14ed0fce863 ] [Swap the precedence of and and or so a conjunction of disjunctions without parentheses groups correctly. David Fox **20100811023748 Ignore-this: cf652fc84b553e454d44b15b63bd3b93 ] [Add Test.New, with six failing tests and some that succeed David Fox **20100810234509 Ignore-this: 6371588b7beac55e760ffb689cc43e19 ] [add a version of clausalNormalForm that returns [[formula], add satisfiable to Logic.Satisfiable David Fox **20100810234152 Ignore-this: 504b693196d10fe84a11faa815fd15da ] [Clean up the exports from Logic.NormalForm David Fox **20100810233126 Ignore-this: bd276b9540bbb409ce503a961b1a0992 ] [Get rid of Show formula super class, rename clauseNormalForm -> clausalNormalForm (to match another branch of logic-haskell) David Fox **20100810231525 Ignore-this: e01a9142186f598b4ffa86a208dd5aeb ] [Add pretty printing, move Boolean to Logic.Logic, add new test module David Fox **20100810181225 Ignore-this: deec8a71608af6ab635eca87ae875ec5 ] [Version 0.18 - remove two synonyms for Formula: Predicate and Proposition David Fox **20100728165004 Ignore-this: 80680b606f3e42a2374bbd2ae7336cf9 ] [Version 0.17 David Fox **20100726150534 Ignore-this: ac95503a7c47283175997d93a9475cef ] [Rename State to ProverState in Logic.Chiou.KnowledgeBase David Fox **20100726145445 Ignore-this: cc401229f2107c11901548432833851e ] [Replace all uses of Chiou normalization functions with fully polymorphic ones David Fox **20100726143552 Ignore-this: f44cf5f4c2cd4adf70af1295c14c0c7c ] [Add a polymorphic skolemize function, eliminate HasSkolem monad class David Fox **20100726141815 Ignore-this: 9dae3d9f7866c871100e8f8459980448 ] [Use moveQuantifiersOut instead of moveQuantifiersLeft, it renames variables properly David Fox **20100726134214 Ignore-this: f44068a32c2756468fad46f07a3039d6 ] [Re-order the normalization functions David Fox **20100726131102 Ignore-this: b11f268a2c15d318cf436d02b608fdd8 ] [Use a more tractable type to compare truth tables, add module name to test case labels David Fox **20100726130710 Ignore-this: 3409ecdbf644274852159aa7ec7a147f ] [Move some normalization functions from Logic.FirstOrder to Logic.Normalize David Fox **20100725171824 Ignore-this: 6666bc3555b95dc15c17652d8b35da53 ] [Show and Eq related stuff David Fox **20100725165626 Ignore-this: a69b57597f36c744c9bdf1df0e49c6de ] [Polymorphic versions of moveQuantifiersLeft, eliminateImplication, moveNotInwards David Fox **20100725134827 Ignore-this: 3243a0f8c41070f3e3cb69d9b0d73dbc ] [Implement a polymorphic version of moveNotInwards David Fox **20100725060508 Ignore-this: 26fef2a1a3574845ced2252b4a8d4dac ] [simplify fromImplicative function in Implicative.hs David Fox **20100725055517 Ignore-this: 1d902c76732d60c561ec76adc186d48 ] [Add Logic.Conjunctive David Fox **20100724065316 Ignore-this: 9075b03d421d0d565a580badf2b1974e ] [Update docs in Implicative David Fox **20100723075334 Ignore-this: 752d8b00b7c255f4413206e069ddb992 ] [Add more parameters and functional dependencies to Implicative class David Fox **20100712201523 Ignore-this: 62cfaa8d6a0821d4476d10e86c1e269c ] [Rename convertPred -> convertFOF, to match class name change David Fox **20100712122820 Ignore-this: 8dfb43919ac6ae260acd6bfca08abb07 ] [Add a toImplicative method to the Implicative class David Fox **20100712122451 Ignore-this: ae2ac997753f2029ea5dd06028eb6a55 ] [Rename some symbols in the Chiou prover that conflict with symbols in FirstOrderLogic David Fox **20100711182719 Ignore-this: 5121d5138023865f5162dc520563c8bb ] [Eliminate the notion of negated literals form the Implicative class, that form doesn't have them David Fox **20100711174535 Ignore-this: d18d1c29f9627ca98bf31bec4fbb75fa ] [Add classes Implicative and Literal in Logic.Implicative, new fromINF implementation David Fox **20100711160241 Ignore-this: c5c40d3585dcce834f2894f0ecb752ca ] [Move the important super classes from the individual functions to the type classes (version 0.16) David Fox **20100711130151 Ignore-this: 325d407f0284d1826f10d732c76da681 ] [Improve docs, add prereqs to FirstOrderLogic class: , Eq p, Boolean p, Eq f, Skolem f David Fox **20100711052239 Ignore-this: 5062ca8eb94a51e0a24cab35e077fbb3 ] [Document the tell function David Fox **20100709202101 Ignore-this: 96f11bee1c9b8ced24bb0e8dcc82e663 ] [Redo the prover functions so they run in the C.ProverT monad David Fox **20100709192628 Ignore-this: c362ee6e742958dfd6c2ab8dfe24df66 ] [Add a Boolean class and require primitive predicates to be an instance, so we can always generate the "always true" and "never true" predicates David Fox **20100709160607 Ignore-this: 3d3ca65a847ee15573974cc71da903a3 ] [Add a Logic.Prover module with a function to load a knowledgebase David Fox **20100709005611 Ignore-this: 7bfa78f433e4a493ce61b1956e1b3f68 ] [Rename PredicateLogic -> FirstOrderLogic David Fox **20100708230054 Ignore-this: 91bc506f36299697211587a29ff1861a ] [Add a missing unit test file David Fox **20100708203828 Ignore-this: d3825bb282d54baf5734bda6e8d17683 ] [Merge chiouprover package into this one David Fox **20100708200503 Ignore-this: ea63dd3d88682f3b45ed2aebf0870b20 ] [Use new fromINF functionfrom the chiouprover package David Fox **20100708180839 Ignore-this: 7754e36ea3fa81e24d1bcf63859a7ce4 ] [Test case stuff, add a note that the AtomicSkolemFunction constructor is redundant David Fox **20100708154700 Ignore-this: bd38a64d58369f92b9461c2537db8fc1 ] [Update dependencies for chiouprover 0.6 David Fox **20100707230814 Ignore-this: 596978c7162baa96dc74d698862cc3c7 ] [Update test suite for chiouprover 0.6 David Fox **20100707230747 Ignore-this: a3780e0e9a745bd0e5c92b1db33fa0bf ] [Version 0.13 David Fox **20100707054018 Ignore-this: e5315682bcfd1d2ec5a81d25815ac8ba ] [Implement implicativeNormalForm and add a test case David Fox **20100707053839 Ignore-this: e147c1470ded1c43e40dc566f8592770 ] [Hide an unused variable David Fox **20100707024043 Ignore-this: 9cce910aab9b8135e92002be651e3190 ] [Change the algorthem for choosing fresh variable names: x -> y -> z -> x2 -> x3 ... David Fox **20100707021020 Ignore-this: a21fdf5629fe6d165331344f7ec5b750 ] [Parameterize the variable type in the Parameterized type and the PredicateLogic class David Fox **20100707005437 Ignore-this: f17637d2c336cc6a75b504f0f65f16cb ] [Remove some lines that upset haddock David Fox **20100706193954 Ignore-this: 294018ddddf0673c85dcd29f972318a4 ] [Import toCNFSentence, update tests, flatten PropForm output to make comparison easier David Fox **20100706192927 Ignore-this: 94962473d6e4101a4c04e410345af838 ] [Modify the tests so they compare the Chiou CNF code with ours David Fox **20100706191205 Ignore-this: f0daef6209e1abb5eb833e31da4032f3 ] [Adding a way to compute cnf via Chiou package, work on polymorphism David Fox **20100706021500 Ignore-this: baf63b2164ce0952d183b3a89b336db7 ] [Change the Skolem class so it uses a monad to generate new skolem variables David Fox **20100705233605 Ignore-this: 47b858df574b2d3f3f603b1a335db38b ] [Add support for the Chiou prover David Fox **20100705172321 Ignore-this: fcdf26a2157b2e80601c04829e30db96 ] [Check in the current state of the unit tests, these will change after the Chiou instances are added David Fox **20100705134920 Ignore-this: 8e1fd1f2b2f80e0b75429ef369bccee9 ] [Small refactoring in Satisfiable module to pull a clauses function out of theorem and related David Fox **20100705134756 Ignore-this: 2d116067cca67155b45896f6bce042b6 ] [Version 0.9 - add the Logic.Satisfiable module David Fox **20100702184016 Ignore-this: 8b342e73796eb3aa42b8fdeb4337c821 ] [Use standard names for the operations in the CNF module David Fox **20100701161144 Ignore-this: b133f6c1835f24d16e062bd32820966c ] [Version 0.8 - cnf should not remove the universal quantifiers, add a removeUniversal that does this and a cnfNoQuants that combines it with cnf David Fox **20100701033533 Ignore-this: 75b8889f128c3be0aad93c6d358d41f1 ] [Change the substitute function so it replaces free occurrences of a V with a term. Before it replaced terms with terms. David Fox **20100630174857 Ignore-this: ecdb40627b0d1d0cc2bb5a050e874bff ] [Re-implement skolemize David Fox **20100630153721 Ignore-this: d579bb720f14a5b74f07f3e549e8a36f ] [Fix a nasty bug in substituteTerm, which is used by skolemize David Fox **20100630134233 Ignore-this: ab34f23079db611961237eb4bbaaba90 ] [Fix the test cases David Fox **20100629184704 Ignore-this: 1a5752f0e693844b977158619f83dfcd ] [Fix a shadowed variable name David Fox **20100629184532 Ignore-this: 403d43308ebc5158246ece1d16defc56 ] [Put more parens into the showForm0 function, maybe too many, but that's better than too few David Fox **20100629170620 Ignore-this: aeeb98a04209a1a8cca68c337a4e4d49 ] [Fix the PropLogic fold function David Fox **20100629170549 Ignore-this: be2d9940e50804e5abb931546f50efca ] [Fix moveQuantifiersIn David Fox **20100629170416 Ignore-this: f5f47113233f3ea10a2a4972e2afd6bd ] [Remove the Show instance for Formula p f so we don't have to have so many Show prereqs David Fox **20100628195938 Ignore-this: c01ee2a4d689377ac09a4cc4a6241260 ] [Add a Skolem v f class to encapsulate conversion of variables to skolem functions David Fox **20100628180721 Ignore-this: 3da6c1ea6de0c7318ae6934df06bc5a6 ] [Eliminate AtomicWord module - we can just use String in the test types now David Fox **20100628150056 Ignore-this: f3a466a383e6675ae172967a803a299e ] [Version 0.6 - Factor a Logic class out of the PropositionalLogic and PredicateLogic classes, eliminates a type variable from PredicateLogic David Fox **20100628145121 Ignore-this: 8a67103a0130fbf738cc987336074499 ] [Version 0.5.1 David Fox **20100627140150 Ignore-this: 90ad1c8ce8891cae1f43c6fbebc99c3f ] [Do variable renaming in moveQuantifiersOut David Fox **20100627135424 Ignore-this: fe3437e9ab1a09a09cf5075f74ad70b ] [Version 0.5 - export distributeDisjuncts David Fox **20100625211357 Ignore-this: bfef1757d37d19bbaddd3fe9ca6ea55e ] [Formatting and documentation David Fox **20100625194615 Ignore-this: 10c888df743b9988afb7459201bbf213 ] [Eliminate (presumably) unicode operators from PredicateLogic type class, they make the amd64 haddock program crash David Fox **20100624204649 Ignore-this: 3817dff7f3cbdb51211221fe11bf7575 ] [Add an Ord instance to AtomicFormula David Fox **20100624170850 Ignore-this: b99d0f873be20e1262cb9d2992a591f ] [Add debian dependencies on proplogic David Fox **20100624150936 Ignore-this: cea156d381d4052aad3319d65422847e ] [Remove bogus tests package from debian/control David Fox **20100624144631 Ignore-this: 8fe1ec28bb1d743ae54ccd7270913f16 ] [Have Logic.Predicate export Logic.Propositional David Fox **20100624144614 Ignore-this: a88f12a8dc59eb626fa4ee6704ec814f ] [Change version to 0.1 David Fox **20100624143943 Ignore-this: 1bec40996be044cc895192f90f5ddd4a ] [Fix bugs in the distributeDisjuncts and convertProp functions, fix test cases David Fox **20100624143048 Ignore-this: 47aeff3ee002f3dd14528326edac661e ] [Rename FirstOrderLogic -> PredicateLogic, split Class module into Propositional and Predicate David Fox **20100624140923 Ignore-this: 948c8de1968c2e7b6a3f08c58ee52fbe ] [Move more functionality from PropositionalLogic to FirstOrderLogic, create a PropLogic instance of PropositionalLogic, test case for conversion to PropLogic David Fox **20100624134543 Ignore-this: 7167a3ea714bcca131336dbee856181b ] [Add a function to convert FirstOrderLogic to PropositionalLogic David Fox **20100623233745 Ignore-this: 3ff2d27e74f156e179709a17989777c8 ] [Add functions to convert between different instances of the Logic classes David Fox **20100623231256 Ignore-this: 2911cedb8c94f963d6fb205641957ea3 ] [Split the Formulae type class into two: PropositionalLogic and FirstOrderLogic David Fox **20100623222336 Ignore-this: c33a0a0fe6408f575d3cf172b2553fed ] [Add debianizatino David Fox **20100623211943 Ignore-this: 3f0ffa60dd08b68780e6c1bed2975c87 ] [Big update David Fox **20100623211827 Ignore-this: 72331a79e71ea70a514884cc4477330b ] [Parameterize the AtomicPredicate type in Formula David Fox **20100618204646 Ignore-this: fcb4690220159f813c8f768eda68436 ] [Initial import David Fox **20100618203455 Ignore-this: 124013f9698cf10c254c184f89f48274 ] Patch bundle hash: 3263984ddf927b1041fa0469c6d1055f3179ebf7