| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.TSTP
- data F = F {}
- data Role
- data Formula
- data Term
- newtype V = V String
- data BinOp
- data InfixPred
- data Quant
- newtype AtomicWord = AtomicWord String
- data Source
- data Rule
- data Parent = Parent String [GTerm]
- isBottom :: F -> Bool
- bottom :: Formula
- freeVarsF :: Formula -> Set V
- freeVarsT :: Term -> Set V
- getFreeVars :: [Formula] -> [V]
- data IntroType
- data Theory
- data Info
- data Status
- data GData
- data GTerm
Documentation
data F
data Role
Formula roles.
Formulas and terms
data Formula
first-order logic formula.
data Term
First-order logic terms.
Constructors
| Var V | Variable |
| NumberLitTerm Rational | Number literal |
| DistinctObjectTerm String | Double-quoted item |
| FunApp AtomicWord [Term] | Function symbol application (constants are encoded as nullary functions) |
Show instances
Formula, Term and other data types in this section
have Show instances that allow pretty-printing
of Formulas and Show [ is an
especial instance that print its contents as
sequence of implicationsFormula]
>>>let f1 = PredApp (AtomicWord "a") []>>>let f2 = PredApp (AtomicWord "b") []>>>let f3 = (BinOp (PredApp (AtomicWord "a") []) (:&:) (PredApp (AtomicWord "b") []))>>>f1a>>>f2b>>>f3a ∧ b>>>[f1,f2,f3]{ a b : Set} → a → b → a ∧ b
Some syntax sugar is also present
>>>PredApp (AtomicWord "$false") []⊥
data BinOp
Binary formula connectives.
data InfixPred
Infix connectives of the form Term -> Term -> Formula.
data Quant
Quantifier specification.
Source information
data Source
Source main purpose is to provide all the information regarding
the deductive process that lead to a given formula. Information
about the rules applied along with parent formulas and
SZS
status are among the information you might expect from this field.
data Rule
Deduction rule applied.
data Parent
Parent formula information.
Functions
getFreeVars :: [Formula] -> [V]
getFreeVars f, given a list of formulas f return all free
variables in the formulas.
Unused types
The following types are required to have full
support of the TSTP syntax but haven't been used yet
in tstp2agda aside from the parser.
data IntroType
Constructors
| Definition_ | |
| AxiomOfChoice | |
| Tautology | |
| Assumption_ | |
| UnknownType |
data Info
Constructors
| Description String | |
| IQuote String | |
| Status Status | |
| Function String [GTerm] | |
| InferenceInfo Rule String [GTerm] | |
| AssumptionR [String] | |
| Refutation Source |
data Status
data GData
Metadata (the general_data rule in TPTP's grammar)