logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Index

 ! 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.Literal fromLiteral Data.Logic.Classes.Literal 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.FirstOrder 2 (Function) Data.Logic.Classes.Literal 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