| ! | Data.Logic.Classes.FirstOrder |
| .!=. | Data.Logic.Classes.Equals |
| .&. | Data.Logic.Classes.Combine |
| .<=. | Data.Logic.Classes.Combine |
| .<=>. | Data.Logic.Classes.Combine |
| .<~>. | Data.Logic.Classes.Combine |
| .=. | Data.Logic.Classes.Equals |
| .=>. | Data.Logic.Classes.Combine |
| .|. | Data.Logic.Classes.Combine |
| .~&. | Data.Logic.Classes.Combine |
| .~. | Data.Logic.Classes.Negate |
| .~|. | Data.Logic.Classes.Combine |
| :&&: | Data.Boolean, Data.Boolean.SatSolver |
| :&: | Data.Logic.Classes.Combine |
| :<=>: | Data.Logic.Classes.Combine |
| :=: | Data.Logic.Types.Harrison.Equal |
| :=>: | Data.Logic.Classes.Combine |
| :|: | Data.Logic.Classes.Combine |
| :||: | Data.Boolean, Data.Boolean.SatSolver |
| :~: | Data.Logic.Classes.Combine |
| <=> | Data.Logic.Classes.Combine |
| ==> | Data.Logic.Classes.Combine |
| ? | Data.Logic.Classes.FirstOrder |
| ai | Data.Logic.Harrison.DefCNF |
| allnonemptysubsets | Data.Logic.Harrison.Lib |
| allpairs | Data.Logic.Harrison.Lib |
| allSatValuations | Data.Logic.Harrison.Prop |
| allsets | Data.Logic.Harrison.Lib |
| allsubsets | Data.Logic.Harrison.Lib |
| allVariables | Data.Logic.Classes.Atom |
| And | |
| 1 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| 3 (Data Constructor) | Data.Logic.Instances.Chiou |
| andcnf | Data.Logic.Harrison.DefCNF |
| andcnf3 | Data.Logic.Harrison.DefCNF |
| antecedent | |
| 1 (Function) | Data.Logic.Harrison.Formulas.Propositional |
| 2 (Function) | Data.Logic.Harrison.Formulas.FirstOrder |
| Apply | |
| 1 (Type/Class) | Data.Logic.Classes.Apply |
| 2 (Data Constructor) | Data.Logic.Types.FirstOrder |
| apply | |
| 1 (Function) | Data.Logic.Harrison.Lib |
| 2 (Function) | Data.Logic.Classes.Apply |
| apply' | Data.Logic.Classes.Apply |
| apply0 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| apply1 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| apply2 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| apply3 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| apply4 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| apply5 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| apply6 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| apply7 | |
| 1 (Function) | Data.Logic.Classes.Apply |
| 2 (Function) | Data.Logic.Classes.Equals |
| applyEq | Data.Logic.Classes.Equals |
| applyEq' | Data.Logic.Classes.Equals |
| Arity | Data.Logic.Classes.Arity |
| arity | Data.Logic.Classes.Arity |
| asBool | Data.Logic.Classes.Constants |
| askKB | Data.Logic.KnowledgeBase |
| askolemize | Data.Logic.Harrison.Skolem |
| assertEqual | Data.Logic.Tests.HUnit |
| Assertion | Data.Logic.Tests.HUnit |
| assertTrue | Data.Boolean.SatSolver |
| assertTrue' | Data.Boolean.SatSolver |
| Atom | |
| 1 (Type/Class) | Data.Logic.Classes.Atom |
| 2 (Data Constructor) | Data.Logic.Types.Propositional |
| 3 (Type/Class) | Data.Logic.Harrison.PropExamples |
| 4 (Type/Class) | Data.Logic.Harrison.DefCNF |
| 5 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 6 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| AtomEq | Data.Logic.Classes.Equals |
| atomic | Data.Logic.Classes.Formula |
| atoms | Data.Logic.Harrison.Prop |
| atom_union | |
| 1 (Function) | Data.Logic.Harrison.Formulas.Propositional |
| 2 (Function) | Data.Logic.Classes.FirstOrder |
| 3 (Function) | Data.Logic.Harrison.Formulas.FirstOrder |
| Bijection | Data.Logic.Types.FirstOrderPublic |
| BinOp | |
| 1 (Type/Class) | Data.Logic.Classes.Combine |
| 2 (Data Constructor) | Data.Logic.Classes.Combine |
| binop | Data.Logic.Classes.Combine |
| Boolean | Data.Boolean, Data.Boolean.SatSolver |
| booleanToCNF | Data.Boolean, Data.Boolean.SatSolver |
| botFixity | Data.Logic.Classes.Pretty |
| branchOnVar | Data.Boolean.SatSolver |
| can | Data.Logic.Harrison.Lib |
| Clause | Data.Boolean, Data.Boolean.SatSolver |
| clauseNormalForm | |
| 1 (Function) | Data.Logic.Classes.Propositional |
| 2 (Function) | Data.Logic.Normal.Clause |
| clauseNormalForm' | Data.Logic.Classes.Propositional |
| clauseNormalFormAlt | Data.Logic.Classes.Propositional |
| clauseNormalFormAlt' | Data.Logic.Classes.Propositional |
| ClauseNormalFormula | Data.Logic.Classes.ClauseNormalForm |
| clauses | Data.Logic.Classes.ClauseNormalForm |
| CNF | |
| 1 (Type/Class) | Data.Boolean, Data.Boolean.SatSolver |
| 2 (Data Constructor) | Data.Logic.Instances.Chiou |
| cnf | Data.Logic.Harrison.Prop |
| cnf' | Data.Logic.Harrison.Prop |
| cnfTrace | Data.Logic.Normal.Clause |
| Combinable | Data.Logic.Classes.Combine |
| Combination | Data.Logic.Classes.Combine |
| Combine | |
| 1 (Data Constructor) | Data.Logic.Types.Propositional |
| 2 (Data Constructor) | Data.Logic.Types.FirstOrder |
| combine | Data.Logic.Classes.Combine, Data.Logic.Classes.Propositional |
| ConjunctiveNormalForm | Data.Logic.Instances.Chiou |
| Connective | |
| 1 (Type/Class) | Data.Logic.Instances.Chiou |
| 2 (Data Constructor) | Data.Logic.Instances.Chiou |
| consequent | |
| 1 (Function) | Data.Logic.Harrison.Formulas.Propositional |
| 2 (Function) | Data.Logic.Harrison.Formulas.FirstOrder |
| Constants | Data.Logic.Classes.Constants |
| contrapositives | Data.Logic.Harrison.Meson |
| convert | Data.Logic.Tests.HUnit |
| convertFOF | Data.Logic.Classes.FirstOrder |
| convertProp | Data.Logic.Classes.Propositional |
| convertTerm | Data.Logic.Classes.Term |
| CTerm | Data.Logic.Instances.Chiou |
| davisputnam | Data.Logic.Harrison.Herbrand |
| davisputnam' | Data.Logic.Harrison.Herbrand |
| deepen | Data.Logic.Harrison.Tableaux |
| defcnf1 | Data.Logic.Harrison.DefCNF |
| defcnf2 | Data.Logic.Harrison.DefCNF |
| defcnf3 | Data.Logic.Harrison.DefCNF |
| defcnfs | Data.Logic.Harrison.DefCNF |
| defined | Data.Logic.Harrison.Lib |
| defstep | Data.Logic.Harrison.DefCNF |
| disjunctiveNormalForm | Data.Logic.Classes.Propositional |
| disjunctiveNormalForm' | Data.Logic.Classes.Propositional |
| Disproved | Data.Logic.KnowledgeBase |
| distrib | Data.Logic.Harrison.Prop |
| distrib' | Data.Logic.Harrison.Lib |
| dnf | Data.Logic.Harrison.Prop |
| dnf' | Data.Logic.Harrison.Prop |
| dnf0 | Data.Logic.Harrison.Prop |
| dpll | Data.Logic.Harrison.DP |
| dp_loop | Data.Logic.Harrison.Herbrand |
| dp_mfn | Data.Logic.Harrison.Herbrand |
| dp_refine | Data.Logic.Harrison.Herbrand |
| dp_refine_loop | Data.Logic.Harrison.Herbrand |
| dual | Data.Logic.Harrison.Prop |
| Equal | |
| 1 (Data Constructor) | Data.Logic.Instances.Chiou |
| 2 (Data Constructor) | Data.Logic.Types.FirstOrder |
| equalitize | Data.Logic.Harrison.Equal |
| EQUALS | Data.Logic.Types.Harrison.Equal |
| Equals | Data.Logic.Classes.Equals |
| equals | Data.Logic.Classes.Equals |
| Equiv | Data.Logic.Instances.Chiou |
| equivalence_axioms | Data.Logic.Harrison.Equal |
| eval | |
| 1 (Function) | Data.Logic.Harrison.Prop |
| 2 (Function) | Data.Logic.Harrison.FOL |
| Exists | |
| 1 (Data Constructor) | Data.Logic.Classes.FirstOrder |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| exists | |
| 1 (Function) | Data.Logic.Harrison.Lib |
| 2 (Function) | Data.Logic.Classes.FirstOrder |
| exists' | Data.Logic.Classes.FirstOrder |
| ExistsCh | Data.Logic.Instances.Chiou |
| F | |
| 1 (Data Constructor) | Data.Logic.Types.Propositional |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 3 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| Failing | Data.Logic.Failing |
| failing | Data.Logic.Failing |
| Failure | Data.Logic.Failing |
| false | Data.Logic.Classes.Constants |
| fApp | Data.Logic.Classes.Term |
| FirstOrderFormula | Data.Logic.Classes.FirstOrder |
| Fixity | |
| 1 (Data Constructor) | Data.Logic.Classes.Pretty |
| 2 (Type/Class) | Data.Logic.Classes.Pretty |
| fixity | Data.Logic.Classes.Pretty |
| FixityDirection | Data.Logic.Classes.Pretty |
| fixityFirstOrder | Data.Logic.Classes.FirstOrder |
| fixityPropositional | Data.Logic.Classes.Propositional |
| flatten | Data.Logic.Instances.PropLogic |
| Fn | Data.Logic.Types.Harrison.FOL |
| FName | Data.Logic.Types.Harrison.FOL |
| FOL | Data.Logic.Types.Harrison.FOL |
| foldApply | Data.Logic.Classes.Apply |
| foldAtomEq | Data.Logic.Classes.Equals |
| foldAtoms | Data.Logic.Classes.Formula |
| foldAtomsFirstOrder | Data.Logic.Classes.FirstOrder |
| foldAtomsLiteral | Data.Logic.Classes.Literal |
| foldAtomsPropositional | Data.Logic.Classes.Propositional |
| foldFirstOrder | Data.Logic.Classes.FirstOrder |
| foldLiteral | Data.Logic.Classes.Literal |
| foldNegation | Data.Logic.Classes.Negate |
| foldPropositional | Data.Logic.Classes.Propositional |
| foldTerm | Data.Logic.Classes.Term |
| foldTerms | Data.Logic.Classes.Atom |
| FOLEQ | Data.Logic.Types.Harrison.Equal |
| ForAll | Data.Logic.Instances.Chiou |
| Forall | |
| 1 (Data Constructor) | Data.Logic.Classes.FirstOrder |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| Formula | |
| 1 (Type/Class) | Data.Logic.Classes.Formula |
| 2 (Type/Class) | Data.Logic.Types.Propositional |
| 3 (Type/Class) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 4 (Type/Class) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| 5 (Type/Class) | Data.Logic.Types.FirstOrder |
| 6 (Type/Class) | Data.Logic.Types.FirstOrderPublic |
| 7 (Data Constructor) | Data.Logic.Types.FirstOrderPublic |
| for_all | Data.Logic.Classes.FirstOrder |
| for_all' | Data.Logic.Classes.FirstOrder |
| fpf | Data.Logic.Harrison.Lib |
| freeVariables | Data.Logic.Classes.Atom |
| fromAtomEq | Data.Logic.Classes.Equals |
| fromBool | Data.Logic.Classes.Constants |
| fromFirstOrder | Data.Logic.Classes.FirstOrder |
| fromLiteral | Data.Logic.Classes.FirstOrder |
| fromSentence | Data.Logic.Instances.Chiou |
| fullUnify | Data.Logic.Harrison.Unif |
| FunApp | Data.Logic.Types.FirstOrder |
| funcs | Data.Logic.Classes.Term |
| funcsAtomEq | Data.Logic.Classes.Equals |
| Function | |
| 1 (Type/Class) | Data.Logic.Classes.Term |
| 2 (Data Constructor) | Data.Logic.Instances.Chiou |
| 3 (Type/Class) | Data.Logic.Types.Harrison.FOL |
| functions | Data.Logic.Harrison.Skolem |
| functions' | Data.Logic.Harrison.Equal |
| function_congruence | Data.Logic.Harrison.Equal |
| fv | Data.Logic.Harrison.FOL |
| fvt | Data.Logic.Classes.Term |
| generalize | Data.Logic.Harrison.FOL |
| getKB | Data.Logic.KnowledgeBase |
| getSetOfSupport | Data.Logic.Resolution |
| getSubst | Data.Logic.Classes.Atom |
| getSubstAtomEq | Data.Logic.Resolution |
| gilmore | Data.Logic.Harrison.Herbrand |
| gilmore_loop | Data.Logic.Harrison.Herbrand |
| groundterms | Data.Logic.Harrison.Herbrand |
| groundtuples | Data.Logic.Harrison.Herbrand |
| HasFixity | Data.Logic.Classes.Pretty |
| herbfuns | Data.Logic.Harrison.Herbrand |
| herbloop | Data.Logic.Harrison.Herbrand |
| ifElse | Data.Logic.Classes.Constants |
| Iff | |
| 1 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| image | Data.Logic.Harrison.Lib |
| Imp | |
| 1 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| ImplicativeForm | Data.Logic.Normal.Implicative |
| implicativeNormalForm | Data.Logic.Normal.Implicative |
| Imply | Data.Logic.Instances.Chiou |
| inconsistant | Data.Logic.Satisfiable |
| inconsistantKB | Data.Logic.KnowledgeBase |
| INF | Data.Logic.Normal.Implicative |
| InfixL | Data.Logic.Classes.Pretty |
| InfixN | Data.Logic.Classes.Pretty |
| InfixR | Data.Logic.Classes.Pretty |
| intern | Data.Logic.Types.FirstOrderPublic |
| Invalid | Data.Logic.KnowledgeBase |
| invalid | Data.Logic.Satisfiable |
| invLiteral | Data.Boolean, Data.Boolean.SatSolver |
| isPositiveLiteral | Data.Boolean, Data.Boolean.SatSolver |
| isRename | Data.Logic.Classes.Atom |
| isRenameOfAtomEq | Data.Logic.Resolution |
| isSkolem | Data.Logic.Classes.Skolem |
| isSolvable | Data.Boolean.SatSolver |
| isSolved | Data.Boolean.SatSolver |
| list_conj | |
| 1 (Function) | Data.Logic.Harrison.Prop |
| 2 (Function) | Data.Logic.Harrison.FOL |
| list_disj | |
| 1 (Function) | Data.Logic.Harrison.Prop |
| 2 (Function) | Data.Logic.Harrison.FOL |
| Literal | |
| 1 (Type/Class) | Data.Boolean, Data.Boolean.SatSolver |
| 2 (Type/Class) | Data.Logic.Classes.Literal |
| LiteralMapT | Data.Logic.Normal.Implicative |
| literalVar | Data.Boolean, Data.Boolean.SatSolver |
| loadKB | Data.Logic.KnowledgeBase |
| lookupVar | Data.Boolean.SatSolver |
| lsimplify | Data.Logic.Harrison.Skolem |
| ma | Data.Logic.Harrison.DefCNF |
| maincnf | Data.Logic.Harrison.DefCNF |
| makeCNF | Data.Logic.Classes.ClauseNormalForm |
| makeINF' | Data.Logic.Normal.Implicative |
| mapAtoms | Data.Logic.Classes.Formula |
| mapAtomsFirstOrder | Data.Logic.Classes.FirstOrder |
| mapAtomsPropositional | Data.Logic.Classes.Propositional |
| mapfilter | Data.Logic.Harrison.Lib |
| match | Data.Logic.Classes.Atom |
| matchAtomsEq | Data.Logic.Harrison.Resolution |
| maximize | Data.Logic.Harrison.Lib |
| maximize' | Data.Logic.Harrison.Lib |
| max_varindex | Data.Logic.Harrison.DefCNF |
| meson | Data.Logic.Harrison.Meson |
| mexpand | Data.Logic.Harrison.Meson |
| minimize | Data.Logic.Harrison.Lib |
| minimize' | Data.Logic.Harrison.Lib |
| mkLits | Data.Logic.Harrison.Prop |
| mkprop | Data.Logic.Harrison.DefCNF |
| mk_defcnf | Data.Logic.Harrison.DefCNF |
| N | Data.Logic.Harrison.PropExamples |
| Named | |
| 1 (Data Constructor) | Data.Logic.Classes.Equals |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Equal |
| Neg | Data.Boolean, Data.Boolean.SatSolver |
| neg | Data.Logic.Normal.Implicative |
| Negatable | Data.Logic.Classes.Negate |
| negate | Data.Logic.Harrison.Prop |
| negated | Data.Logic.Classes.Negate |
| negatePrivate | Data.Logic.Classes.Negate |
| negationNormalForm | Data.Logic.Classes.Propositional |
| negative | |
| 1 (Function) | Data.Logic.Classes.Negate |
| 2 (Function) | Data.Logic.Harrison.Prop |
| nenf | Data.Logic.Harrison.Prop |
| newSatSolver | Data.Boolean.SatSolver |
| NFEqual | Data.Logic.Instances.Chiou |
| NFNot | Data.Logic.Instances.Chiou |
| NFPredicate | Data.Logic.Instances.Chiou |
| nnf | |
| 1 (Function) | Data.Logic.Harrison.Prop |
| 2 (Function) | Data.Logic.Harrison.Skolem |
| No | Data.Boolean, Data.Boolean.SatSolver |
| NormalFunction | Data.Logic.Instances.Chiou |
| NormalSentence | Data.Logic.Instances.Chiou |
| NormalT | Data.Logic.Normal.Implicative |
| NormalTerm | Data.Logic.Instances.Chiou |
| NormalVariable | Data.Logic.Instances.Chiou |
| Not | |
| 1 (Data Constructor) | Data.Boolean, Data.Boolean.SatSolver |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 3 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| 4 (Data Constructor) | Data.Logic.Instances.Chiou |
| NumAtom | Data.Logic.Harrison.DefCNF |
| onAllValuations | Data.Logic.Harrison.Prop |
| onatoms | Data.Logic.Classes.FirstOrder |
| on_atoms | |
| 1 (Function) | Data.Logic.Harrison.Formulas.Propositional |
| 2 (Function) | Data.Logic.Harrison.Formulas.FirstOrder |
| optimize | Data.Logic.Harrison.Lib |
| optimize' | Data.Logic.Harrison.Lib |
| Or | |
| 1 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| 3 (Data Constructor) | Data.Logic.Instances.Chiou |
| orcnf | Data.Logic.Harrison.DefCNF |
| overatoms | |
| 1 (Function) | Data.Logic.Classes.Propositional |
| 2 (Function) | Data.Logic.Classes.FirstOrder |
| over_atoms | |
| 1 (Function) | Data.Logic.Harrison.Formulas.Propositional |
| 2 (Function) | Data.Logic.Harrison.Formulas.FirstOrder |
| P | |
| 1 (Data Constructor) | Data.Logic.Harrison.PropExamples |
| 2 (Data Constructor) | Data.Logic.Harrison.DefCNF |
| 3 (Data Constructor) | Data.Logic.Types.Harrison.Prop |
| pApp | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp0 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp1 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp2 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp3 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp4 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp5 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp6 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pApp7 | |
| 1 (Function) | Data.Logic.Classes.FirstOrder |
| 2 (Function) | Data.Logic.Classes.Equals |
| pholds | Data.Logic.Harrison.Herbrand |
| plSat | Data.Logic.Instances.PropLogic |
| plSat0 | Data.Logic.Instances.PropLogic |
| pname | Data.Logic.Types.Harrison.Prop |
| pnf | Data.Logic.Harrison.Skolem |
| Pos | Data.Boolean, Data.Boolean.SatSolver |
| pos | Data.Logic.Normal.Implicative |
| positive | |
| 1 (Function) | Data.Logic.Classes.Negate |
| 2 (Function) | Data.Logic.Harrison.Prop |
| Predicate | |
| 1 (Type/Class) | Data.Logic.Classes.Apply |
| 2 (Data Constructor) | Data.Logic.Instances.Chiou |
| 3 (Type/Class) | Data.Logic.Types.FirstOrder |
| 4 (Data Constructor) | Data.Logic.Types.FirstOrder |
| PredicateName | Data.Logic.Classes.Equals |
| predicates | Data.Logic.Harrison.Equal |
| predicate_congruence | Data.Logic.Harrison.Equal |
| PredName | Data.Logic.Types.Harrison.Equal |
| prefix | Data.Logic.Classes.Variable |
| presolution | Data.Logic.Harrison.Resolution |
| Pretty | Data.Logic.Classes.Pretty |
| pretty | Data.Logic.Classes.Pretty |
| prettyApply | Data.Logic.Classes.Apply |
| prettyAtomEq | Data.Logic.Classes.Equals |
| prettyBinOp | Data.Logic.Classes.Combine |
| prettyBool | Data.Logic.Classes.Constants |
| prettyFirstOrder | Data.Logic.Classes.FirstOrder |
| prettyINF | Data.Logic.Normal.Implicative |
| prettyLit | Data.Logic.Classes.Literal |
| prettyProof | Data.Logic.Normal.Implicative |
| prettyPropositional | Data.Logic.Classes.Propositional |
| prettyTerm | Data.Logic.Classes.Term |
| prettyVariable | Data.Logic.Classes.Variable |
| prime | Data.Logic.Harrison.PropExamples |
| Proof | |
| 1 (Type/Class) | Data.Logic.KnowledgeBase |
| 2 (Data Constructor) | Data.Logic.KnowledgeBase |
| proof | Data.Logic.KnowledgeBase |
| ProofResult | Data.Logic.KnowledgeBase |
| proofResult | Data.Logic.KnowledgeBase |
| Prop | Data.Logic.Types.Harrison.Prop |
| PropositionalFormula | Data.Logic.Classes.Propositional |
| prove | Data.Logic.Resolution |
| Proved | Data.Logic.KnowledgeBase |
| ProverT | Data.Logic.KnowledgeBase |
| psimplify | Data.Logic.Harrison.Prop |
| pSubst | Data.Logic.Harrison.Prop |
| PTerm | Data.Logic.Types.FirstOrder |
| public | Data.Logic.Types.FirstOrderPublic |
| purednf | Data.Logic.Harrison.Prop |
| puremeson | Data.Logic.Harrison.Meson |
| Quant | |
| 1 (Type/Class) | Data.Logic.Classes.FirstOrder |
| 2 (Data Constructor) | Data.Logic.Types.FirstOrder |
| quant | Data.Logic.Classes.FirstOrder |
| quant' | Data.Logic.Classes.FirstOrder |
| Quantifier | |
| 1 (Type/Class) | Data.Logic.Instances.Chiou |
| 2 (Data Constructor) | Data.Logic.Instances.Chiou |
| R | |
| 1 (Data Constructor) | Data.Logic.Types.Harrison.FOL |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Equal |
| ramsey | Data.Logic.Harrison.PropExamples |
| rawdnf | Data.Logic.Harrison.Prop |
| renamerule | Data.Logic.Harrison.Prolog |
| resolution1 | Data.Logic.Harrison.Resolution |
| resolution2 | Data.Logic.Harrison.Resolution |
| resolution3 | Data.Logic.Harrison.Resolution |
| runNormal | Data.Logic.Normal.Implicative |
| runNormalT | Data.Logic.Normal.Implicative |
| runProver' | Data.Logic.KnowledgeBase |
| runProverT' | Data.Logic.KnowledgeBase |
| runSkolem | Data.Logic.Harrison.Skolem |
| runSkolemT | Data.Logic.Harrison.Skolem |
| satisfiable | |
| 1 (Function) | Data.Logic.Classes.ClauseNormalForm |
| 2 (Function) | Data.Logic.Harrison.Prop |
| 3 (Function) | Data.Logic.Satisfiable |
| SatSolver | Data.Boolean.SatSolver |
| selectBranchVar | Data.Boolean.SatSolver |
| Sentence | Data.Logic.Instances.Chiou |
| setAll | Data.Logic.Harrison.Lib |
| setAny | Data.Logic.Harrison.Lib |
| setmapfilter | Data.Logic.Harrison.Lib |
| SetOfSupport | Data.Logic.Resolution |
| settryfind | Data.Logic.Harrison.Lib |
| showApply | Data.Logic.Classes.Apply |
| showAtomEq | Data.Logic.Classes.Equals |
| showFirstOrder | Data.Logic.Classes.FirstOrder |
| showFirstOrderFormulaEq | Data.Logic.Classes.Equals |
| showKB | Data.Logic.KnowledgeBase |
| showPropositional | Data.Logic.Classes.Propositional |
| showTerm | Data.Logic.Classes.Term |
| showVariable | Data.Logic.Classes.Variable |
| simpcnf | |
| 1 (Function) | Data.Logic.Harrison.Prop |
| 2 (Function) | Data.Logic.Harrison.Normal |
| simpcnf' | Data.Logic.Harrison.Normal |
| simpdnf | |
| 1 (Function) | Data.Logic.Harrison.Prop |
| 2 (Function) | Data.Logic.Harrison.Normal |
| simpdnf' | Data.Logic.Harrison.Normal |
| simplify | Data.Logic.Harrison.Skolem |
| Skolem | |
| 1 (Type/Class) | Data.Logic.Classes.Skolem |
| 2 (Type/Class) | Data.Logic.Harrison.Skolem |
| 3 (Data Constructor) | Data.Logic.Types.Harrison.FOL |
| skolem | Data.Logic.Harrison.Skolem |
| skolemize | Data.Logic.Harrison.Skolem |
| skolemNormalForm | Data.Logic.Harrison.Skolem |
| SkolemT | Data.Logic.Harrison.Skolem |
| solve | |
| 1 (Function) | Data.Boolean.SatSolver |
| 2 (Function) | Data.Logic.Harrison.Unif |
| specialize | Data.Logic.Harrison.Skolem |
| subcnf | Data.Logic.Harrison.DefCNF |
| subst | Data.Logic.Harrison.FOL |
| subst' | Data.Logic.Harrison.Herbrand |
| substApply | Data.Logic.Classes.Apply |
| substAtomEq | Data.Logic.Classes.Equals |
| substitute | Data.Logic.Classes.Atom |
| Success | Data.Logic.Failing |
| T | |
| 1 (Data Constructor) | Data.Logic.Types.Propositional |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.Propositional |
| 3 (Data Constructor) | Data.Logic.Types.Harrison.Formulas.FirstOrder |
| tautology | Data.Logic.Harrison.Prop |
| tellKB | Data.Logic.KnowledgeBase |
| Term | Data.Logic.Classes.Term |
| TermType | Data.Logic.Types.Harrison.FOL |
| Test | Data.Logic.Tests.HUnit |
| Test0 | Data.Logic.Tests.HUnit |
| TestCase | Data.Logic.Tests.HUnit |
| TestFormula | Data.Logic.Tests.HUnit |
| TestFormulaEq | Data.Logic.Tests.HUnit |
| TestLabel | Data.Logic.Tests.HUnit |
| TestList | Data.Logic.Tests.HUnit |
| tests | |
| 1 (Function) | Data.Logic.Harrison.Lib |
| 2 (Function) | Data.Logic.Harrison.PropExamples |
| 3 (Function) | Data.Logic.Harrison.DP |
| theorem | Data.Logic.Satisfiable |
| theoremKB | Data.Logic.KnowledgeBase |
| toCNF | Data.Logic.Instances.SatSolver |
| toLiteral | Data.Logic.Instances.SatSolver |
| topFixity | Data.Logic.Classes.Pretty |
| toPropositional | |
| 1 (Function) | Data.Logic.Classes.Literal |
| 2 (Function) | Data.Logic.Classes.FirstOrder |
| toSentence | Data.Logic.Instances.Chiou |
| toSkolem | Data.Logic.Classes.Skolem |
| trivial | |
| 1 (Function) | Data.Logic.Harrison.Prop |
| 2 (Function) | Data.Logic.Harrison.Normal |
| true | Data.Logic.Classes.Constants |
| TruthTable | Data.Logic.Harrison.Prop |
| truthTable | Data.Logic.Harrison.Prop |
| TruthTableRow | Data.Logic.Harrison.Prop |
| tryApplyD | Data.Logic.Harrison.Lib |
| tryfind | Data.Logic.Harrison.Lib |
| tsubst | Data.Logic.Classes.Term |
| unFormula | Data.Logic.Types.FirstOrderPublic |
| Unification | Data.Logic.Resolution |
| unify | |
| 1 (Function) | Data.Logic.Classes.Atom |
| 2 (Function) | Data.Logic.Harrison.Unif |
| unifyAndApply | Data.Logic.Harrison.Unif |
| unifyAtomsEq | Data.Logic.Harrison.Tableaux |
| unify_literals | Data.Logic.Harrison.Tableaux |
| unloadKB | Data.Logic.KnowledgeBase |
| unsatisfiable | Data.Logic.Harrison.Prop |
| validKB | Data.Logic.KnowledgeBase |
| Var | |
| 1 (Data Constructor) | Data.Boolean, Data.Boolean.SatSolver |
| 2 (Data Constructor) | Data.Logic.Types.Harrison.FOL |
| 3 (Data Constructor) | Data.Logic.Types.FirstOrder |
| var | Data.Logic.Harrison.FOL |
| varApply | Data.Logic.Classes.Apply |
| varAtomEq | Data.Logic.Classes.Equals |
| Variable | |
| 1 (Type/Class) | Data.Logic.Classes.Variable |
| 2 (Data Constructor) | Data.Logic.Instances.Chiou |
| variant | Data.Logic.Classes.Variable |
| variants | Data.Logic.Classes.Variable |
| vt | Data.Logic.Classes.Term |
| wiIdent | Data.Logic.KnowledgeBase |
| wiItem | Data.Logic.KnowledgeBase |
| WithId | |
| 1 (Type/Class) | Data.Logic.KnowledgeBase |
| 2 (Data Constructor) | Data.Logic.KnowledgeBase |
| withUnivQuants | Data.Logic.Classes.FirstOrder |
| Yes | Data.Boolean, Data.Boolean.SatSolver |
| zipApplys | Data.Logic.Classes.Apply |
| zipAtomsEq | Data.Logic.Classes.Equals |
| zipFirstOrder | Data.Logic.Classes.FirstOrder |
| zipLiterals | Data.Logic.Classes.Literal |
| zipTerms | Data.Logic.Classes.Term |
| |-> | Data.Logic.Harrison.Lib |
| |=> | Data.Logic.Harrison.Lib |
| ¬ | Data.Logic.Classes.Negate |
| ⇒ | Data.Logic.Classes.Combine |
| ⇔ | Data.Logic.Classes.Combine |
| ∀ | Data.Logic.Classes.FirstOrder |
| ∃ | Data.Logic.Classes.FirstOrder |
| ∅ | Data.Logic.Harrison.Lib |
| ∧ | Data.Logic.Classes.Combine |
| ∨ | Data.Logic.Classes.Combine |
| ≡ | Data.Logic.Classes.Equals |
| ≢ | Data.Logic.Classes.Equals |
| ⊨ | Data.Logic.Classes.Constants |
| ⊭ | Data.Logic.Classes.Constants |