Index
| /\ | ATP.FOL, ATP |
| <=> | ATP.FOL, ATP |
| <~> | ATP.FOL, ATP |
| =/= | ATP.FOL, ATP |
| === | ATP.FOL, ATP |
| ==> | ATP.FOL, ATP |
| ?= | ATP.FOL, ATP |
| addSequent | ATP.FOL, ATP |
| Alpha | ATP.FOL, ATP |
| alpha | ATP.FOL, ATP |
| AlphaT | ATP.FOL, ATP |
| And | ATP.FOL, ATP |
| antecedents | ATP.FOL, ATP |
| Atomic | ATP.FOL, ATP |
| Axiom | ATP.FOL, ATP |
| AxiomOfChoice | ATP.FOL, ATP |
| axioms | ATP.FOL, ATP |
| BackwardDemodulation | ATP.FOL, ATP |
| BinaryFunction | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| BinaryPredicate | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| Binder | ATP.FOL, ATP |
| binding | ATP.FOL, ATP |
| bound | ATP.FOL, ATP |
| boundIn | ATP.FOL, ATP |
| breadthFirst | ATP.FOL, ATP |
| Claim | ATP.FOL, ATP |
| Clause | |
| 1 (Data Constructor) | ATP.FOL, ATP |
| 2 (Type/Class) | ATP.FOL, ATP |
| clause | ATP.FOL, ATP |
| Clauses | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| clauses | ATP.FOL, ATP |
| Clausification | ATP.FOL, ATP |
| close | ATP.FOL, ATP |
| closed | ATP.FOL, ATP |
| Conjecture | ATP.FOL, ATP |
| conjecture | ATP.FOL, ATP |
| Conjunction | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| conjunction | ATP.FOL, ATP |
| Connected | ATP.FOL, ATP |
| Connective | ATP.FOL, ATP |
| consequent | ATP.FOL, ATP |
| Constant | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| Contradiction | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| debug | ATP.Prove, ATP |
| decode | ATP.Codec.TPTP |
| decodeClause | ATP.Codec.TPTP |
| decodeFormula | ATP.Codec.TPTP |
| decodeSolution | ATP.Codec.TPTP |
| defaultOptions | ATP.Prove, ATP |
| defaultProver | ATP.Prover, ATP |
| Derivation | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| Disjunction | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| disjunction | ATP.FOL, ATP |
| E | ATP.Prover, ATP |
| EmptyClause | ATP.FOL, ATP |
| encode | ATP.Codec.TPTP |
| encodeClause | ATP.Codec.TPTP |
| encodeClauses | ATP.Codec.TPTP |
| encodeFormula | ATP.Codec.TPTP |
| encodeTheorem | ATP.Codec.TPTP |
| EnnfTransformation | ATP.FOL, ATP |
| enter | ATP.FOL, ATP |
| eprover | ATP.Prover, ATP |
| Equality | ATP.FOL, ATP |
| Equivalence | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| equivalence | ATP.FOL, ATP |
| Equivalent | ATP.FOL, ATP |
| Error | ATP.Error, ATP |
| evalAlpha | ATP.FOL, ATP |
| evalAlphaT | ATP.FOL, ATP |
| executable | ATP.Prover, ATP |
| Exists | ATP.FOL, ATP |
| exists | ATP.FOL, ATP |
| ExitCodeError | ATP.Error, ATP |
| exitCodeError | ATP.Error, ATP |
| Falsity | ATP.FOL, ATP |
| FalsityLiteral | ATP.FOL, ATP |
| FirstOrder | ATP.FOL, ATP |
| flattenConjunction | ATP.FOL, ATP |
| flattenDisjunction | ATP.FOL, ATP |
| Flattening | ATP.FOL, ATP |
| Forall | ATP.FOL, ATP |
| forall | ATP.FOL, ATP |
| Formula | |
| 1 (Data Constructor) | ATP.FOL, ATP |
| 2 (Type/Class) | ATP.FOL, ATP |
| ForwardDemodulation | ATP.FOL, ATP |
| free | ATP.FOL, ATP |
| freeIn | ATP.FOL, ATP |
| Function | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| FunctionSymbol | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| getClauses | ATP.FOL, ATP |
| getConjunction | ATP.FOL, ATP |
| getDisjunction | ATP.FOL, ATP |
| getEquivalence | ATP.FOL, ATP |
| getInequivalence | ATP.FOL, ATP |
| getLiterals | ATP.FOL, ATP |
| ground | ATP.FOL, ATP |
| hprint | ATP.Pretty.FOL, ATP |
| Implies | ATP.FOL, ATP |
| Inequivalence | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| inequivalence | ATP.FOL, ATP |
| Inference | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| inferenceRule | ATP.FOL, ATP |
| isAssociative | ATP.FOL, ATP |
| isFailure | ATP.Error, ATP |
| isSuccess | ATP.Error, ATP |
| labeling | ATP.FOL, ATP |
| liftClause | ATP.FOL, ATP |
| liftContradiction | ATP.FOL, ATP |
| liftPartial | ATP.Error, ATP |
| liftRefutation | ATP.FOL, ATP |
| liftSignedLiteral | ATP.FOL, ATP |
| Literal | ATP.FOL, ATP |
| Literals | ATP.FOL, ATP |
| LogicalExpression | ATP.FOL, ATP |
| lookup | ATP.FOL, ATP |
| MemoryLimit | ATP.Prover, ATP |
| memoryLimit | ATP.Prove, ATP |
| MemoryLimitError | ATP.Error, ATP |
| memoryLimitError | ATP.Error, ATP |
| MonadAlpha | ATP.FOL, ATP |
| neg | ATP.FOL, ATP |
| Negate | ATP.FOL, ATP |
| NegatedConjecture | ATP.FOL, ATP |
| Negative | ATP.FOL, ATP |
| NnfTransformation | ATP.FOL, ATP |
| NoClauses | ATP.FOL, ATP |
| occurrence | ATP.FOL, ATP |
| occursIn | ATP.FOL, ATP |
| Or | ATP.FOL, ATP |
| Other | ATP.FOL, ATP |
| OtherError | ATP.Error, ATP |
| otherError | ATP.Error, ATP |
| Paramodulation | ATP.FOL, ATP |
| ParsingError | ATP.Error, ATP |
| parsingError | ATP.Error, ATP |
| Partial | ATP.Error, ATP |
| PartialT | |
| 1 (Type/Class) | ATP.Error, ATP |
| 2 (Data Constructor) | ATP.Error, ATP |
| Positive | ATP.FOL, ATP |
| pprint | ATP.Pretty.FOL, ATP |
| Predicate | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| PredicateSymbol | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| Pretty | ATP.Pretty.FOL, ATP |
| pretty | ATP.Pretty.FOL, ATP |
| prettyList | ATP.Pretty.FOL, ATP |
| Proof | ATP.FOL, ATP |
| ProofError | ATP.Error, ATP |
| proofError | ATP.Error, ATP |
| Proposition | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| Propositional | ATP.FOL, ATP |
| prove | ATP.Prove, ATP |
| Prover | |
| 1 (Type/Class) | ATP.Prover, ATP |
| 2 (Data Constructor) | ATP.Prover, ATP |
| prover | ATP.Prove, ATP |
| proverArguments | ATP.Prover, ATP |
| proverOutput | ATP.Prover, ATP |
| proveUsing | ATP.Prove, ATP |
| proveWith | ATP.Prove, ATP |
| ProvingOptions | |
| 1 (Type/Class) | ATP.Prove, ATP |
| 2 (Data Constructor) | ATP.Prove, ATP |
| Quantified | ATP.FOL, ATP |
| quantified | ATP.FOL, ATP |
| Quantifier | ATP.FOL, ATP |
| Refutation | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| refute | ATP.Prove, ATP |
| refuteUsing | ATP.Prove, ATP |
| refuteWith | ATP.Prove, ATP |
| Resolution | ATP.FOL, ATP |
| Rule | ATP.FOL, ATP |
| RuleName | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| ruleName | ATP.FOL, ATP |
| runPartialT | ATP.Error, ATP |
| Saturation | ATP.FOL, ATP |
| scope | ATP.FOL, ATP |
| Sequent | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| share | ATP.FOL, ATP |
| Sign | ATP.FOL, ATP |
| sign | ATP.FOL, ATP |
| Signed | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| signed | ATP.FOL, ATP |
| signof | ATP.FOL, ATP |
| Simplify | ATP.FOL, ATP |
| simplify | ATP.FOL, ATP |
| SingleClause | ATP.FOL, ATP |
| singleClause | ATP.FOL, ATP |
| Skolemisation | ATP.FOL, ATP |
| Solution | ATP.FOL, ATP |
| SubsumptionResolution | ATP.FOL, ATP |
| Superposition | ATP.FOL, ATP |
| Tautology | ATP.FOL, ATP |
| TautologyClause | ATP.FOL, ATP |
| TautologyLiteral | ATP.FOL, ATP |
| Term | ATP.FOL, ATP |
| TernaryFunction | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| TernaryPredicate | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| Theorem | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| TimeLimit | ATP.Prover, ATP |
| timeLimit | ATP.Prove, ATP |
| TimeLimitError | ATP.Error, ATP |
| timeLimitError | ATP.Error, ATP |
| TrivialInequality | ATP.FOL, ATP |
| UnaryFunction | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| UnaryPredicate | |
| 1 (Type/Class) | ATP.FOL, ATP |
| 2 (Data Constructor) | ATP.FOL, ATP |
| UnitClause | ATP.FOL, ATP |
| unitClause | ATP.FOL, ATP |
| Unknown | ATP.FOL, ATP |
| unliftClause | ATP.FOL, ATP |
| unliftContradiction | ATP.FOL, ATP |
| unliftRefutation | ATP.FOL, ATP |
| unliftSignedLiteral | ATP.FOL, ATP |
| unprefix | ATP.FOL, ATP |
| unRuleName | ATP.FOL, ATP |
| unsign | ATP.FOL, ATP |
| Vampire | ATP.Prover, ATP |
| vampire | ATP.Prover, ATP |
| Var | ATP.FOL, ATP |
| Variable | ATP.FOL, ATP |
| vars | ATP.FOL, ATP |
| Vendor | ATP.Prover, ATP |
| vendor | ATP.Prover, ATP |
| Xor | ATP.FOL, ATP |
| \/ | ATP.FOL, ATP |
| |- | ATP.FOL, ATP |
| ~= | ATP.FOL, ATP |