tstp2agda-0.1.0.0: Proof-term reconstruction from TSTP to Agda

Data.TSTP

Synopsis

Documentation

data F

Main formula type, it contains all the elements and information of a TSTP formula definition. While name, role, and formula are self-explanatory, source is a messy meta-language in itself, different ATPs may embed different amounts of information in it.

Constructors

 F Fieldsname :: String role :: Role formula :: Formula source :: Source

Instances

 Eq F Ord F Read F Show F

data Role

Formula roles.

Instances

 Eq Role Ord Role Read Role Show Role

Formulas and terms

data Formula

first-order logic formula.

Constructors

 BinOp Formula BinOp Formula Binary connective application InfixPred Term InfixPred Term Infix predicate application PredApp AtomicWord [Term] Predicate application Quant Quant [V] Formula Quantified Formula (:~:) Formula Negation

Instances

 Eq Formula Ord Formula Read Formula Show Formula Show [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)

Instances

 Eq Term Ord Term Read Term Show Term

Show instances

Formula, Term and other data types in this section have Show instances that allow pretty-printing of Formulas and Show [Formula] is an especial instance that print its contents as sequence of implications

>>> let f1 = PredApp (AtomicWord "a") []
>>> let f2 = PredApp (AtomicWord "b") []
>>> let f3 = (BinOp (PredApp (AtomicWord "a") []) (:&:) (PredApp (AtomicWord "b") []))
>>> f1
a
>>> f2
b
>>> f3
a ∧ b
>>> [f1,f2,f3]
{ a b : Set} → a → b → a ∧ b

Some syntax sugar is also present

>>> PredApp (AtomicWord "\$false") []

newtype V

Variable

Constructors

 V String

Instances

 Eq V Ord V Read V Show V

data BinOp

Binary formula connectives.

Constructors

 (:<=>:) ↔ Equivalence (:=>:) → Implication (:<=:) ← Reverse Implication (:&:) ∧ AND (:|:) ∨ OR (:~&:) ⊼ NAND (:~|:) ⊽ NOR (:<~>:) ⊕ XOR

Instances

 Eq BinOp Ord BinOp Read BinOp Show BinOp

data InfixPred

Infix connectives of the form Term -> Term -> Formula.

Constructors

 (:=:) = (:!=:) ≠

Instances

 Eq InfixPred Ord InfixPred Read InfixPred Show InfixPred

data Quant

Quantifier specification.

Constructors

 All ∀ Exists ∃

Instances

 Eq Quant Ord Quant Read Quant Show Quant

newtype AtomicWord

Constructors

 AtomicWord String

Instances

 Eq AtomicWord Ord AtomicWord Read AtomicWord Show AtomicWord

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.

Constructors

 Source String Inference Rule [Info] [Parent] Introduced IntroType [Info] File String (Maybe String) Theory Theory [Info] Creator String [Info] Name String NoSource

Instances

 Eq Source Ord Source Read Source Show Source

data Rule

Deduction rule applied.

Constructors

 Simplify Negate Canonicalize Strip NewRule String

Instances

 Eq Rule Ord Rule Read Rule Show Rule

data Parent

Parent formula information.

Constructors

 Parent String [GTerm]

Instances

 Eq Parent Ord Parent Read Parent Show Parent

Functions

isBottom :: F -> Bool

isBottom f, test whether f = ⊥.

bottom = ⊥.

freeVarsF f, returns a Set of all free variables of f.

freeVarsT t, returns a Set of all free variables of t.

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

Instances

 Eq IntroType Ord IntroType Read IntroType Show IntroType

data Theory

Constructors

 Equality AC

Instances

 Eq Theory Ord Theory Read Theory Show Theory

data Info

Constructors

 Description String IQuote String Status Status Function String [GTerm] InferenceInfo Rule String [GTerm] AssumptionR [String] Refutation Source

Instances

 Eq Info Ord Info Read Info Show Info

data Status

Constructors

 Suc Unp Sap Esa Sat Fsa Thm Eqv Tac Wec Eth Tau Wtc Wth Cax Sca Tca Wca Cup Csp Ecs Csa Cth Ceq Unc Wcc Ect Fun Uns Wuc Wct Scc Uca Noc Unk

Instances

 Eq Status Ord Status Read Status Show Status

data GData

Metadata (the general_data rule in TPTP's grammar)

Instances

 Eq GData Ord GData Read GData Show GData

data GTerm

Metadata (the general_term rule in TPTP's grammar)

Constructors

 ColonSep GData GTerm GTerm GData GList [GTerm]

Instances

 Eq GTerm Ord GTerm Read GTerm Show GTerm