Index
| $$ | Data.Logic.ATP |
| $+$ | Data.Logic.ATP |
| .&. | Data.Logic.ATP.Prop, Data.Logic.ATP |
| .<=>. | Data.Logic.ATP.Prop, Data.Logic.ATP |
| .=. | Data.Logic.ATP.Equate, Data.Logic.ATP |
| .=>. | Data.Logic.ATP.Prop, Data.Logic.ATP |
| .|. | Data.Logic.ATP.Prop, Data.Logic.ATP |
| .~. | Data.Logic.ATP.Lit, Data.Logic.ATP |
| :!: | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| :&: | Data.Logic.ATP.Prop, Data.Logic.ATP |
| :<=>: | Data.Logic.ATP.Prop, Data.Logic.ATP |
| :=>: | Data.Logic.ATP.Prop, Data.Logic.ATP |
| :?: | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| :|: | Data.Logic.ATP.Prop, Data.Logic.ATP |
| <+> | Data.Logic.ATP |
| <==> | Data.Logic.ATP.Prop, Data.Logic.ATP |
| <=> | Data.Logic.ATP.Prop, Data.Logic.ATP |
| <> | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| ==> | Data.Logic.ATP.Prop, Data.Logic.ATP |
| @=? | Data.Logic.ATP |
| @? | Data.Logic.ATP |
| @?= | Data.Logic.ATP |
| ai | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| allIds | Data.Logic.ATP.Parser, Data.Logic.ATP |
| allnonemptysubsets | Data.Logic.ATP.Lib, Data.Logic.ATP |
| allOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| allpairs | Data.Logic.ATP.Lib, Data.Logic.ATP |
| allsatvaluations | Data.Logic.ATP.Prop, Data.Logic.ATP |
| allsets | Data.Logic.ATP.Lib, Data.Logic.ATP |
| allsubsets | Data.Logic.ATP.Lib, Data.Logic.ATP |
| And | |
| 1 (Data Constructor) | Data.Logic.ATP.Prop |
| 2 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| andOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| andPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| AP | Data.Logic.ATP.Apply, Data.Logic.ATP |
| ApAtom | Data.Logic.ATP.Apply, Data.Logic.ATP |
| ApFormula | Data.Logic.ATP.FOL, Data.Logic.ATP |
| apply | Data.Logic.ATP.Lib, Data.Logic.ATP |
| applyPredicate | Data.Logic.ATP.Apply, Data.Logic.ATP |
| Arity | Data.Logic.ATP.Term, Data.Logic.ATP |
| asBool | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| askolemize | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| assert | Data.Logic.ATP |
| Assertable | Data.Logic.ATP |
| assertBool | Data.Logic.ATP |
| assertEqual | Data.Logic.ATP |
| assertEqual' | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| assertFailure | Data.Logic.ATP |
| Assertion | Data.Logic.ATP |
| AssertionPredicable | Data.Logic.ATP |
| AssertionPredicate | Data.Logic.ATP |
| assertionPredicate | Data.Logic.ATP |
| assertString | Data.Logic.ATP |
| Associativity | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| associativity | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| associativityEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| associativityLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| associativityPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| associativityQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| associativityTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| asubst | Data.Logic.ATP.FOL, Data.Logic.ATP |
| Atom | |
| 1 (Data Constructor) | Data.Logic.ATP.Lit |
| 2 (Data Constructor) | Data.Logic.ATP.Prop |
| 3 (Type/Class) | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| 4 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| atomFuncs | Data.Logic.ATP.Apply, Data.Logic.ATP |
| atomic | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| AtomOf | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| atomPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| atoms | Data.Logic.ATP.Prop, Data.Logic.ATP |
| atom_union | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| BinOp | Data.Logic.ATP.Prop, Data.Logic.ATP |
| binop | Data.Logic.ATP.Prop, Data.Logic.ATP |
| boolPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| bool_interp | Data.Logic.ATP.FOL, Data.Logic.ATP |
| braces | Data.Logic.ATP |
| brackets | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| can | Data.Logic.ATP.Lib, Data.Logic.ATP |
| cases | Data.Logic.ATP |
| cat | Data.Logic.ATP |
| char | Data.Logic.ATP |
| Chr | Data.Logic.ATP |
| cnf' | Data.Logic.ATP.Prop, Data.Logic.ATP |
| cnf_ | Data.Logic.ATP.Prop, Data.Logic.ATP |
| colon | Data.Logic.ATP |
| comma | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| compete | Data.Logic.ATP.Lib, Data.Logic.ATP |
| constants | Data.Logic.ATP.Parser, Data.Logic.ATP |
| convertApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| convertEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| convertLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| convertPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| convertQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| convertTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| convertToLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| convertToPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| Counts | |
| 1 (Data Constructor) | Data.Logic.ATP |
| 2 (Type/Class) | Data.Logic.ATP |
| counts | Data.Logic.ATP |
| davisputnam | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| davisputnam' | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| davis_putnam_example_formula | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| deepen | Data.Logic.ATP.Lib, Data.Logic.ATP |
| def | Data.Logic.ATP.Parser, Data.Logic.ATP |
| defcnf1 | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| defcnf2 | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| defcnf3 | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| defcnfs | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| defined | Data.Logic.ATP.Lib, Data.Logic.ATP |
| Depth | |
| 1 (Type/Class) | Data.Logic.ATP.Lib, Data.Logic.ATP |
| 2 (Data Constructor) | Data.Logic.ATP.Lib, Data.Logic.ATP |
| distrib | Data.Logic.ATP.Lib, Data.Logic.ATP |
| dnf | Data.Logic.ATP.Prop, Data.Logic.ATP |
| dnfSet | Data.Logic.ATP.Prop, Data.Logic.ATP |
| Doc | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| double | Data.Logic.ATP |
| doubleQuotes | Data.Logic.ATP |
| dp | Data.Logic.ATP.DP, Data.Logic.ATP |
| dplb | Data.Logic.ATP.DP, Data.Logic.ATP |
| dplbsat | Data.Logic.ATP.DP, Data.Logic.ATP |
| dplbtaut | Data.Logic.ATP.DP, Data.Logic.ATP |
| dpli | Data.Logic.ATP.DP, Data.Logic.ATP |
| dplisat | Data.Logic.ATP.DP, Data.Logic.ATP |
| dplitaut | Data.Logic.ATP.DP, Data.Logic.ATP |
| dpll | Data.Logic.ATP.DP, Data.Logic.ATP |
| dpllsat | Data.Logic.ATP.DP, Data.Logic.ATP |
| dplltaut | Data.Logic.ATP.DP, Data.Logic.ATP |
| dpsat | Data.Logic.ATP.DP, Data.Logic.ATP |
| dptaut | Data.Logic.ATP.DP, Data.Logic.ATP |
| dp_loop | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| dp_mfn | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| dp_refine | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| dp_refine_loop | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| dual | Data.Logic.ATP.Prop, Data.Logic.ATP |
| empty | Data.Logic.ATP |
| entailsOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| EqAtom | Data.Logic.ATP.Equate, Data.Logic.ATP |
| EqFormula | Data.Logic.ATP.FOL, Data.Logic.ATP |
| eqPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| equalitize | Data.Logic.ATP.Equal, Data.Logic.ATP |
| Equals | Data.Logic.ATP.Equate, Data.Logic.ATP |
| equals | Data.Logic.ATP |
| equate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| equateOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| errors | Data.Logic.ATP |
| eval | Data.Logic.ATP.Prop, Data.Logic.ATP |
| evalRS | Data.Logic.ATP.Lib, Data.Logic.ATP |
| existentialQuantifier | Data.Logic.ATP.Parser, Data.Logic.ATP |
| Exists | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| exists | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| existsIds | Data.Logic.ATP.Parser, Data.Logic.ATP |
| existsOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| F | |
| 1 (Data Constructor) | Data.Logic.ATP.Lit |
| 2 (Data Constructor) | Data.Logic.ATP.Prop |
| 3 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| Failing | Data.Logic.ATP.Lib, Data.Logic.ATP |
| failing | Data.Logic.ATP.Lib, Data.Logic.ATP |
| Failure | Data.Logic.ATP.Lib, Data.Logic.ATP |
| failures | Data.Logic.ATP |
| false | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| falseIds | Data.Logic.ATP.Parser, Data.Logic.ATP |
| falseOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| fApp | Data.Logic.ATP.Term, Data.Logic.ATP |
| FApply | Data.Logic.ATP.Term, Data.Logic.ATP |
| fcat | Data.Logic.ATP |
| first | Data.Logic.ATP |
| flatten | Data.Logic.ATP.Lib, Data.Logic.ATP |
| float | Data.Logic.ATP |
| Fn | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| FName | |
| 1 (Type/Class) | Data.Logic.ATP.Term, Data.Logic.ATP |
| 2 (Data Constructor) | Data.Logic.ATP.Term, Data.Logic.ATP |
| fof | Data.Logic.ATP.Parser, Data.Logic.ATP |
| FOL | Data.Logic.ATP.Equate, Data.Logic.ATP |
| FOLAP | Data.Logic.ATP.Apply, Data.Logic.ATP |
| folconstant | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folconstant_numeric | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folconstant_reserved | Data.Logic.ATP.Parser, Data.Logic.ATP |
| foldApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| foldApply' | Data.Logic.ATP.Apply, Data.Logic.ATP |
| foldCombination | Data.Logic.ATP.Prop, Data.Logic.ATP |
| foldEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| foldLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| foldLiteral' | Data.Logic.ATP.Lit, Data.Logic.ATP |
| foldNegation | Data.Logic.ATP.Lit, Data.Logic.ATP |
| foldPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| foldPropositional' | Data.Logic.ATP.Prop, Data.Logic.ATP |
| foldQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| foldSkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| foldTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| folfunction | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folfunction_infix | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folparser | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folpredicate | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folpredicate_infix | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folsubterm | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folsubterm_prefix | Data.Logic.ATP.Parser, Data.Logic.ATP |
| folterm | Data.Logic.ATP.Parser, Data.Logic.ATP |
| Forall | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| forallIds | Data.Logic.ATP.Parser, Data.Logic.ATP |
| forallOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| forallQuantifier | Data.Logic.ATP.Parser, Data.Logic.ATP |
| Formula | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| for_all | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| fpf | Data.Logic.ATP.Lib, Data.Logic.ATP |
| fromBool | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| fsep | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| FTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| fullRender | Data.Logic.ATP |
| fullunify | Data.Logic.ATP.Unif, Data.Logic.ATP |
| funcs | Data.Logic.ATP.Term, Data.Logic.ATP |
| Function | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| functions | Data.Logic.ATP.Apply, Data.Logic.ATP |
| function_congruence | Data.Logic.ATP.Equal, Data.Logic.ATP |
| FunOf | Data.Logic.ATP.Term, Data.Logic.ATP |
| fv | Data.Logic.ATP.FOL, Data.Logic.ATP |
| fva | Data.Logic.ATP.FOL, Data.Logic.ATP |
| fvt | Data.Logic.ATP.FOL, Data.Logic.ATP |
| generalize | Data.Logic.ATP.FOL, Data.Logic.ATP |
| gilmore | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| gilmore_loop | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| groundterms | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| groundtuples | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| hang | Data.Logic.ATP |
| HasApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| HasEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| HasFixity | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| HasSkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| hcat | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| herbfuns | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| herbloop | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| holds | Data.Logic.ATP.FOL, Data.Logic.ATP |
| holdsAtom | Data.Logic.ATP.FOL, Data.Logic.ATP |
| holdsQuantified | Data.Logic.ATP.FOL, Data.Logic.ATP |
| hsep | Data.Logic.ATP |
| Iff | |
| 1 (Data Constructor) | Data.Logic.ATP.Prop |
| 2 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| iffOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| iffPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| image | Data.Logic.ATP.Lib, Data.Logic.ATP |
| Imp | |
| 1 (Data Constructor) | Data.Logic.ATP.Prop |
| 2 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| impOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| impPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| InfixA | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| InfixL | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| InfixN | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| InfixR | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| int | Data.Logic.ATP |
| integer | Data.Logic.ATP |
| Interp | Data.Logic.ATP.FOL, Data.Logic.ATP |
| IsAtom | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| isEmpty | Data.Logic.ATP |
| IsFirstOrder | Data.Logic.ATP.FOL, Data.Logic.ATP |
| IsFormula | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| IsFunction | Data.Logic.ATP.Term, Data.Logic.ATP |
| IsLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| IsPredicate | Data.Logic.ATP.Apply, Data.Logic.ATP |
| IsPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| IsQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| IsTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| IsVariable | Data.Logic.ATP.Term, Data.Logic.ATP |
| JL | Data.Logic.ATP.LitWrapper |
| JustApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| JustLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| JustPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| K | |
| 1 (Data Constructor) | Data.Logic.ATP.PropExamples |
| 2 (Type/Class) | Data.Logic.ATP.Tableaux |
| 3 (Data Constructor) | Data.Logic.ATP.Tableaux |
| Knows | Data.Logic.ATP.PropExamples, Data.Logic.ATP |
| L | Data.Logic.ATP.Lit, Data.Logic.ATP |
| Label | Data.Logic.ATP |
| lbrace | Data.Logic.ATP |
| lbrack | Data.Logic.ATP |
| leafPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| LeftMode | Data.Logic.ATP |
| LFormula | Data.Logic.ATP.Lit, Data.Logic.ATP |
| LHS | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| lineLength | Data.Logic.ATP |
| listAssert | Data.Logic.ATP |
| ListAssertable | Data.Logic.ATP |
| ListItem | Data.Logic.ATP |
| list_conj | Data.Logic.ATP.Prop, Data.Logic.ATP |
| list_disj | Data.Logic.ATP.Prop, Data.Logic.ATP |
| Lit | Data.Logic.ATP.Lit, Data.Logic.ATP |
| lit | Data.Logic.ATP.Parser, Data.Logic.ATP |
| litexprparser | Data.Logic.ATP.Parser, Data.Logic.ATP |
| litparser | Data.Logic.ATP.Parser, Data.Logic.ATP |
| litterm | Data.Logic.ATP.Parser, Data.Logic.ATP |
| lname | Data.Logic.ATP.Lit, Data.Logic.ATP |
| Location | |
| 1 (Data Constructor) | Data.Logic.ATP |
| 2 (Type/Class) | Data.Logic.ATP |
| locationColumn | Data.Logic.ATP |
| locationFile | Data.Logic.ATP |
| locationLine | Data.Logic.ATP |
| lparen | Data.Logic.ATP |
| lsubst | Data.Logic.ATP.FOL, Data.Logic.ATP |
| ma | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| mapfilter | Data.Logic.ATP.Lib, Data.Logic.ATP |
| match_atoms | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| match_atoms_eq | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| maximize | Data.Logic.ATP.Lib, Data.Logic.ATP |
| maybeBraces | Data.Logic.ATP |
| maybeBrackets | Data.Logic.ATP |
| maybeDoubleQuotes | Data.Logic.ATP |
| maybeParens | Data.Logic.ATP |
| maybeQuotes | Data.Logic.ATP |
| meson | Data.Logic.ATP.Meson, Data.Logic.ATP |
| meson1 | Data.Logic.ATP.Meson, Data.Logic.ATP |
| meson2 | Data.Logic.ATP.Meson, Data.Logic.ATP |
| minimize | Data.Logic.ATP.Lib, Data.Logic.ATP |
| mk_knows | Data.Logic.ATP.PropExamples, Data.Logic.ATP |
| mk_knows2 | Data.Logic.ATP.PropExamples, Data.Logic.ATP |
| mk_lits | Data.Logic.ATP.Prop, Data.Logic.ATP |
| Mode | Data.Logic.ATP |
| mode | Data.Logic.ATP |
| mod_interp | Data.Logic.ATP.FOL, Data.Logic.ATP |
| m_angles | Data.Logic.ATP.Parser, Data.Logic.ATP |
| m_identifier | Data.Logic.ATP.Parser, Data.Logic.ATP |
| m_integer | Data.Logic.ATP.Parser, Data.Logic.ATP |
| m_parens | Data.Logic.ATP.Parser, Data.Logic.ATP |
| m_reserved | Data.Logic.ATP.Parser, Data.Logic.ATP |
| m_reservedOp | Data.Logic.ATP.Parser, Data.Logic.ATP |
| m_symbol | Data.Logic.ATP.Parser, Data.Logic.ATP |
| m_whiteSpace | Data.Logic.ATP.Parser, Data.Logic.ATP |
| N | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| naiveNegate | Data.Logic.ATP.Lit, Data.Logic.ATP |
| negate | Data.Logic.ATP.Lit, Data.Logic.ATP |
| negated | Data.Logic.ATP.Lit, Data.Logic.ATP |
| negative | Data.Logic.ATP.Lit, Data.Logic.ATP |
| nenf | Data.Logic.ATP.Prop, Data.Logic.ATP |
| nest | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| nnf | |
| 1 (Function) | Data.Logic.ATP.Prop |
| 2 (Function) | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| Node | Data.Logic.ATP |
| Not | |
| 1 (Data Constructor) | Data.Logic.ATP.Lit |
| 2 (Data Constructor) | Data.Logic.ATP.Prop |
| 3 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| notOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| notPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| NumAtom | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| onallvaluations | Data.Logic.ATP.Prop, Data.Logic.ATP |
| onatoms | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| onatomsLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| onatomsPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| onatomsQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| OneLineMode | Data.Logic.ATP |
| onformula | Data.Logic.ATP.Apply, Data.Logic.ATP |
| onterms | Data.Logic.ATP.Apply, Data.Logic.ATP |
| ontermsApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| ontermsEq | Data.Logic.ATP.Equate, Data.Logic.ATP |
| optimize | Data.Logic.ATP.Lib, Data.Logic.ATP |
| Or | |
| 1 (Data Constructor) | Data.Logic.ATP.Prop |
| 2 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| orOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| orPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| overatoms | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| overatomsLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| overatomsPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| overatomsQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| overterms | Data.Logic.ATP.Apply, Data.Logic.ATP |
| overtermsApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| overtermsEq | Data.Logic.ATP.Equate, Data.Logic.ATP |
| P | Data.Logic.ATP.Prop, Data.Logic.ATP |
| p24 | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| p45 | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| p45fm | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| PageMode | Data.Logic.ATP |
| pApp | Data.Logic.ATP.Apply, Data.Logic.ATP |
| pAppPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| parens | Data.Logic.ATP |
| parseFOL | Data.Logic.ATP.Parser, Data.Logic.ATP |
| parseFOL' | Data.Logic.ATP.ParserTests |
| parseFOLTerm | Data.Logic.ATP.Parser, Data.Logic.ATP |
| parseLit | Data.Logic.ATP.Parser, Data.Logic.ATP |
| parsePL | Data.Logic.ATP.Parser, Data.Logic.ATP |
| Path | Data.Logic.ATP |
| path | Data.Logic.ATP |
| performTest | Data.Logic.ATP |
| pf | Data.Logic.ATP.Parser, Data.Logic.ATP |
| PFormula | Data.Logic.ATP.Prop, Data.Logic.ATP |
| pholds | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| pname | Data.Logic.ATP.Prop, Data.Logic.ATP |
| pnf | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| positive | Data.Logic.ATP.Lit, Data.Logic.ATP |
| pPrint | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| pPrintList | Data.Logic.ATP |
| pPrintPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| prawitz | Data.Logic.ATP.Tableaux, Data.Logic.ATP |
| Precedence | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| precedence | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| precedenceEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| precedenceLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| precedencePropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| precedenceQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| precedenceTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| Predicate | Data.Logic.ATP.Apply, Data.Logic.ATP |
| predicate_infix_symbols | Data.Logic.ATP.Parser, Data.Logic.ATP |
| PredOf | Data.Logic.ATP.Apply, Data.Logic.ATP |
| prefix | Data.Logic.ATP.Term, Data.Logic.ATP |
| presolution | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| Pretty | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| prettyApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| prettyBool | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| prettyEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| prettyFoldable | Data.Logic.ATP.Lib, Data.Logic.ATP |
| prettyFunctionApply | Data.Logic.ATP.Term, Data.Logic.ATP |
| PrettyLevel | |
| 1 (Data Constructor) | Data.Logic.ATP |
| 2 (Type/Class) | Data.Logic.ATP |
| prettyLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| prettyNormal | Data.Logic.ATP |
| prettyParen | Data.Logic.ATP |
| prettyPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| prettyQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| prettyShow | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| prettySkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| prettyTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| prime | Data.Logic.ATP.PropExamples, Data.Logic.ATP |
| Prolog | Data.Logic.ATP.Prolog, Data.Logic.ATP |
| PrologRule | Data.Logic.ATP.Prolog, Data.Logic.ATP |
| Prop | Data.Logic.ATP.Prop, Data.Logic.ATP |
| propexprparser | Data.Logic.ATP.Parser, Data.Logic.ATP |
| propparser | Data.Logic.ATP.Parser, Data.Logic.ATP |
| propterm | Data.Logic.ATP.Parser, Data.Logic.ATP |
| provesOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| psimplify | Data.Logic.ATP.Prop, Data.Logic.ATP |
| psimplify1 | Data.Logic.ATP.Prop, Data.Logic.ATP |
| PStr | Data.Logic.ATP |
| psubst | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ptext | Data.Logic.ATP |
| punctuate | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| purecnf | Data.Logic.ATP.Prop, Data.Logic.ATP |
| purednf | Data.Logic.ATP.Prop, Data.Logic.ATP |
| PutText | |
| 1 (Data Constructor) | Data.Logic.ATP |
| 2 (Type/Class) | Data.Logic.ATP |
| putTextToHandle | Data.Logic.ATP |
| putTextToShowS | Data.Logic.ATP |
| QFormula | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| Quant | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| quant | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| quantifierId | Data.Logic.ATP.Parser, Data.Logic.ATP |
| quantifierOp | Data.Logic.ATP.Parser, Data.Logic.ATP |
| quantPrec | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| quotes | Data.Logic.ATP |
| R | Data.Logic.ATP.Equate, Data.Logic.ATP |
| ramsey | Data.Logic.ATP.PropExamples, Data.Logic.ATP |
| rational | Data.Logic.ATP |
| rawdnf | Data.Logic.ATP.Prop, Data.Logic.ATP |
| rbrace | Data.Logic.ATP |
| rbrack | Data.Logic.ATP |
| reduceDoc | Data.Logic.ATP |
| renamerule | Data.Logic.ATP.Prolog, Data.Logic.ATP |
| render | Data.Logic.ATP |
| renderStyle | Data.Logic.ATP |
| ReportProblem | Data.Logic.ATP |
| ReportStart | Data.Logic.ATP |
| resolution1 | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| resolution2 | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| resolution3 | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| RHS | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| ribbonsPerLine | Data.Logic.ATP |
| rparen | Data.Logic.ATP |
| runRS | Data.Logic.ATP.Lib, Data.Logic.ATP |
| runSkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| runSkolemT | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| runTestText | Data.Logic.ATP |
| runTestTT | Data.Logic.ATP |
| satisfiable | Data.Logic.ATP.Prop, Data.Logic.ATP |
| semi | Data.Logic.ATP |
| sep | Data.Logic.ATP |
| setAll | Data.Logic.ATP.Lib, Data.Logic.ATP |
| setAny | Data.Logic.ATP.Lib, Data.Logic.ATP |
| SetLike | Data.Logic.ATP.Lib, Data.Logic.ATP |
| setmapfilter | Data.Logic.ATP.Lib, Data.Logic.ATP |
| settryfind | Data.Logic.ATP.Lib, Data.Logic.ATP |
| showApply | Data.Logic.ATP.Apply, Data.Logic.ATP |
| showApplyAndEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| showCounts | Data.Logic.ATP |
| showEquate | Data.Logic.ATP.Equate, Data.Logic.ATP |
| showFunctionApply | Data.Logic.ATP.Term, Data.Logic.ATP |
| showLiteral | Data.Logic.ATP.Lit, Data.Logic.ATP |
| showPath | Data.Logic.ATP |
| showPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| showQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| showSkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| showTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| Side | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| simpcnf | Data.Logic.ATP.Prop, Data.Logic.ATP |
| simpcnf' | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| simpdnf | Data.Logic.ATP.Prop, Data.Logic.ATP |
| simpdnf' | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| simplify | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| sizedText | Data.Logic.ATP |
| SkAtom | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| Skolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| skolemize | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| SkolemM | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| skolems | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| SkolemT | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| SkTerm | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| slEmpty | Data.Logic.ATP.Lib, Data.Logic.ATP |
| slInsert | Data.Logic.ATP.Lib, Data.Logic.ATP |
| slMap | Data.Logic.ATP.Lib, Data.Logic.ATP |
| slSingleton | Data.Logic.ATP.Lib, Data.Logic.ATP |
| slUnion | Data.Logic.ATP.Lib, Data.Logic.ATP |
| slView | Data.Logic.ATP.Lib, Data.Logic.ATP |
| solve | Data.Logic.ATP.Unif, Data.Logic.ATP |
| space | Data.Logic.ATP |
| specialize | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| State | |
| 1 (Data Constructor) | Data.Logic.ATP |
| 2 (Type/Class) | Data.Logic.ATP |
| Str | Data.Logic.ATP |
| Style | |
| 1 (Data Constructor) | Data.Logic.ATP |
| 2 (Type/Class) | Data.Logic.ATP |
| style | Data.Logic.ATP |
| subst | Data.Logic.ATP.FOL, Data.Logic.ATP |
| substq | Data.Logic.ATP.FOL, Data.Logic.ATP |
| Success | Data.Logic.ATP.Lib, Data.Logic.ATP |
| SVarOf | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| T | |
| 1 (Data Constructor) | Data.Logic.ATP.Lit |
| 2 (Data Constructor) | Data.Logic.ATP.Prop |
| 3 (Data Constructor) | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| t | Data.Logic.ATP.ParserTests |
| tab | Data.Logic.ATP.Tableaux, Data.Logic.ATP |
| tautology | Data.Logic.ATP.Prop, Data.Logic.ATP |
| Term | Data.Logic.ATP.Term, Data.Logic.ATP |
| term | Data.Logic.ATP.Parser, Data.Logic.ATP |
| TermOf | Data.Logic.ATP.Apply, Data.Logic.ATP |
| termval | Data.Logic.ATP.FOL, Data.Logic.ATP |
| Test | Data.Logic.ATP |
| test | Data.Logic.ATP |
| test01 | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| Testable | Data.Logic.ATP |
| TestCase | Data.Logic.ATP |
| testCaseCount | Data.Logic.ATP |
| testCasePaths | Data.Logic.ATP |
| testDefCNF | Data.Logic.ATP.DefCNF, Data.Logic.ATP |
| testDP | Data.Logic.ATP.DP, Data.Logic.ATP |
| testEqual | Data.Logic.ATP.Equal, Data.Logic.ATP |
| testEquals | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| testFOL | Data.Logic.ATP.FOL, Data.Logic.ATP |
| testHerbrand | Data.Logic.ATP.Herbrand, Data.Logic.ATP |
| TestLabel | Data.Logic.ATP |
| testLib | Data.Logic.ATP.Lib, Data.Logic.ATP |
| TestList | Data.Logic.ATP |
| testMeson | Data.Logic.ATP.Meson, Data.Logic.ATP |
| testParen | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| testParser | Data.Logic.ATP.ParserTests |
| testProlog | Data.Logic.ATP.Prolog, Data.Logic.ATP |
| testProp | Data.Logic.ATP.Prop, Data.Logic.ATP |
| testPropExamples | Data.Logic.ATP.PropExamples, Data.Logic.ATP |
| testResolution | Data.Logic.ATP.Resolution, Data.Logic.ATP |
| testSkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| testTableaux | Data.Logic.ATP.Tableaux, Data.Logic.ATP |
| testTerm | Data.Logic.ATP.Term, Data.Logic.ATP |
| testUnif | Data.Logic.ATP.Unif, Data.Logic.ATP |
| text | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| TextDetails | Data.Logic.ATP |
| time | Data.Logic.ATP.Lib, Data.Logic.ATP |
| timeComputation | Data.Logic.ATP.Lib, Data.Logic.ATP |
| timeMessage | Data.Logic.ATP.Lib, Data.Logic.ATP |
| timeout | Data.Logic.ATP.Lib, Data.Logic.ATP |
| Top | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| toSkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| tried | Data.Logic.ATP |
| trivial | Data.Logic.ATP.Prop, Data.Logic.ATP |
| true | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| trueIds | Data.Logic.ATP.Parser, Data.Logic.ATP |
| trueOps | Data.Logic.ATP.Parser, Data.Logic.ATP |
| TruthTable | |
| 1 (Type/Class) | Data.Logic.ATP.Prop, Data.Logic.ATP |
| 2 (Data Constructor) | Data.Logic.ATP.Prop, Data.Logic.ATP |
| truthTable | Data.Logic.ATP.Prop, Data.Logic.ATP |
| tryApplyD | Data.Logic.ATP.Lib, Data.Logic.ATP |
| tryfind | Data.Logic.ATP.Lib, Data.Logic.ATP |
| tryfindM | Data.Logic.ATP.Lib, Data.Logic.ATP |
| tsubst | Data.Logic.ATP.FOL, Data.Logic.ATP |
| TVarOf | Data.Logic.ATP.Term, Data.Logic.ATP |
| Unary | Data.Logic.ATP.Pretty, Data.Logic.ATP |
| undefine | Data.Logic.ATP.Lib, Data.Logic.ATP |
| Unify | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unify | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unify' | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unify_and_apply | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unify_atoms | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unify_atoms_eq | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unify_literals | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unify_terms | Data.Logic.ATP.Unif, Data.Logic.ATP |
| unJL | Data.Logic.ATP.LitWrapper |
| unsatisfiable | Data.Logic.ATP.Prop, Data.Logic.ATP |
| UTermOf | Data.Logic.ATP.Unif, Data.Logic.ATP |
| V | |
| 1 (Type/Class) | Data.Logic.ATP.Term, Data.Logic.ATP |
| 2 (Data Constructor) | Data.Logic.ATP.Term, Data.Logic.ATP |
| Var | Data.Logic.ATP.Term, Data.Logic.ATP |
| var | Data.Logic.ATP.FOL, Data.Logic.ATP |
| variant | Data.Logic.ATP.Term, Data.Logic.ATP |
| variants | Data.Logic.ATP.Term, Data.Logic.ATP |
| variantSkolem | Data.Logic.ATP.Skolem, Data.Logic.ATP |
| VarOf | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| vcat | Data.Logic.ATP |
| vt | Data.Logic.ATP.Term, Data.Logic.ATP |
| wishnu | Data.Logic.ATP.Equal, Data.Logic.ATP |
| zeroWidthText | Data.Logic.ATP |
| ZigZagMode | Data.Logic.ATP |
| zipApplys | Data.Logic.ATP.Apply, Data.Logic.ATP |
| zipEquates | Data.Logic.ATP.Equate, Data.Logic.ATP |
| zipLiterals | Data.Logic.ATP.Lit, Data.Logic.ATP |
| zipLiterals' | Data.Logic.ATP.Lit, Data.Logic.ATP |
| zipPropositional | Data.Logic.ATP.Prop, Data.Logic.ATP |
| zipQuantified | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| zipTerms | Data.Logic.ATP.Term, Data.Logic.ATP |
| |-> | Data.Logic.ATP.Lib, Data.Logic.ATP |
| |=> | Data.Logic.ATP.Lib, Data.Logic.ATP |
| ~: | Data.Logic.ATP |
| ~=? | Data.Logic.ATP |
| ~? | Data.Logic.ATP |
| ~?= | Data.Logic.ATP |
| ¬ | Data.Logic.ATP.Lit, Data.Logic.ATP |
| · | Data.Logic.ATP.Prop, Data.Logic.ATP |
| → | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ↔ | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ⇒ | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ⇔ | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ∀ | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| ∃ | Data.Logic.ATP.Quantified, Data.Logic.ATP |
| ∅ | Data.Logic.ATP.Lib, Data.Logic.ATP |
| ∧ | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ∨ | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ⊃ | Data.Logic.ATP.Prop, Data.Logic.ATP |
| ⊤ | Data.Logic.ATP.Formulas, Data.Logic.ATP |
| ⊥ | Data.Logic.ATP.Formulas, Data.Logic.ATP |