logic-TPTP-0.2.0.7: Import, export etc. for TPTP, a syntax for first-order logic

Codec.TPTP.Base

Contents

Synopsis

Basic undecorated formulae and terms

type Formula = F IdentitySource

Basic (undecorated) first-order formulae

type Term = T IdentitySource

Basic (undecorated) terms

Formulae and terms decoreated with state

type FormulaST s = F (State s)Source

First-order formulae decorated with state

type TermST s = T (State s)Source

Terms decorated with state

type FormulaC = FormulaST [String]Source

First-order formulae decorated with comments

type TermC = TermST [String]Source

Terms decorated with comments

forgetFC :: FormulaC -> FormulaSource

Forget comments in formulae decoreated with comments

forgetTC :: TermC -> TermSource

Forget comments in terms decoreated with comments

(.<=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

Equivalence

Don't let the type context of these wrapper function confuse you :) -- the important special case is just:

(.<=>.) :: Formula -> Formula -> Formula

(.=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

Implication

(.<=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

Reverse implication

(.|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

Disjunction/OR

(.&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

Conjunction/AND

(.<~>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

XOR

(.~|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

NOR

(.~&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F c -> F cSource

NAND

(.~.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => F c -> F cSource

Negation

(.=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => T c -> T c -> F cSource

Equality

(.!=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => T c -> T c -> F cSource

Inequality

for_all :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> F c -> F cSource

Universal quantification

exists :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> F c -> F cSource

Existential quantification

pApp :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => AtomicWord -> [T c] -> F cSource

Predicate symbol application

var :: Pointed (Term0 (T c)) (c (Term0 (T c))) => V -> T cSource

Variable

fApp :: Pointed (Term0 (T c)) (c (Term0 (T c))) => AtomicWord -> [T c] -> T cSource

Function symbol application (constants are encoded as nullary functions)

numberLitTerm :: Pointed (Term0 (T c)) (c (Term0 (T c))) => Double -> T cSource

Number literal

distinctObjectTerm :: Pointed (Term0 (T c)) (c (Term0 (T c))) => String -> T cSource

Double-quoted string literal, called Distinct Object in TPTP's grammar

General decorated formulae and terms

data Formula0 term formula Source

See http://haskell.org/haskellwiki/Indirect_composite for the point of the type parameters (they allow for future decorations, e.g. monadic subformulae). If you don't need decorations, you can just use Formula and the wrapped constructors above.

Constructors

BinOp formula BinOp formula

Binary connective application

InfixPred term InfixPred term

Infix predicate application (equalities, inequalities)

PredApp AtomicWord [term]

Predicate application

Quant Quant [V] formula

Quantified formula

:~: formula

Negation

Instances

Typeable2 Formula0 
(Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f)) 
(Eq term, Eq formula) => Eq (Formula0 term formula) 
(Data term, Data formula) => Data (Formula0 term formula) 
(Ord term, Ord formula) => Ord (Formula0 term formula) 
(Read term, Read formula) => Read (Formula0 term formula) 
(Show term, Show formula) => Show (Formula0 term formula) 
(Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b) 
Pretty (Formula0 Term Formula) 
(ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f) 

data Term0 term Source

See http://haskell.org/haskellwiki/Indirect_composite for the point of the type parameters (they allow for future decorations). If you don't need decorations, you can just use Term and the wrapped constructors above.

Constructors

Var V

Variable

NumberLitTerm Double

Number literal

DistinctObjectTerm String

Double-quoted item

FunApp AtomicWord [term]

Function symbol application (constants are encoded as nullary functions)

Instances

Typeable1 Term0 
Eq term => Eq (Term0 term) 
Data term => Data (Term0 term) 
Ord term => Ord (Term0 term) 
Read term => Read (Term0 term) 
Show term => Show (Term0 term) 
Arbitrary a => Arbitrary (Term0 a) 
Pretty (Term0 Term) 
Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t)) 
ToTPTP t => ToTPTP (Term0 t) 

newtype F c Source

Formulae whose subexpressions are wrapped in the given type constructor c.

For example:

  • c = Identity: Plain formulae
  • c = Maybe: Formulae that may contain "holes"
  • c = IORef: (Mutable) formulae with mutable subexpressions

Constructors

F 

Fields

runF :: c (Formula0 (T c) (F c))
 

Instances

Diffable Formula (F DiffResult) 
Eq (c (Formula0 (T c) (F c))) => Eq (F c) 
(Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (F c) 
Ord (c (Formula0 (T c) (F c))) => Ord (F c) 
Read (c (Formula0 (T c) (F c))) => Read (F c) 
Show (c (Formula0 (T c) (F c))) => Show (F c) 
Show (F DiffResult) 
Typeable1 c => Typeable (F c) 
Pretty (F Identity) 
Pretty (F DiffResult) 
Pretty (WithEnclosing (F DiffResult)) 
ToTPTP (F Identity) 

newtype T c Source

Terms whose subterms are wrapped in the given type constructor c

Constructors

T 

Fields

runT :: c (Term0 (T c))
 

Instances

Diffable Term (T DiffResult) 
Eq (c (Term0 (T c))) => Eq (T c) 
(Typeable1 c, Data (c (Term0 (T c)))) => Data (T c) 
Ord (c (Term0 (T c))) => Ord (T c) 
Read (c (Term0 (T c))) => Read (T c) 
Show (c (Term0 (T c))) => Show (T c) 
Show (T DiffResult) 
Typeable1 c => Typeable (T c) 
Pretty (T Identity) 
Pretty (T DiffResult) 
Pretty (WithEnclosing (T DiffResult)) 
ToTPTP (T Identity) 

data BinOp Source

Binary formula connectives

Constructors

:<=>:

Equivalence

:=>:

Implication

:<=:

Reverse Implication

:&:

AND

:|:

OR

:~&:

NAND

:~|:

NOR

:<~>:

XOR

data Quant Source

Quantifier specification

Constructors

All 
Exists 

Formula Metadata

type TPTP_Input = TPTP_Input_ IdentitySource

A line of a TPTP file: Annotated formula, comment or include statement.

type TPTP_Input_C = TPTP_Input_ (State [String])Source

A line of a TPTP file: Annotated formula (with the comment string embbeded in the State monad ), comment or include statement

data TPTP_Input_ c Source

generalized TPTP_Input -- problem deriving Data and Typable instance TODO other than that backward compatible

Constructors

AFormula

Annotated formulae

Comment String 
Include FilePath [AtomicWord] 

Instances

Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c) 
Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c) 
Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c) 
Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c) 

data Role Source

Formula roles -- why isn't this newtype??

Constructors

Role 

Fields

unrole :: String
 

data GTerm Source

Metadata (the general_term rule in TPTP's grammar)

Gathering free Variables

class FreeVars a whereSource

Methods

freeVars :: a -> Set VSource

Obtain the free variables from a formula or term

univquant_free_vars :: Formula -> FormulaSource

Universally quantify all free variables in the formula

newtype AtomicWord Source

TPTP constant symbol/predicate symbol/function symbol identifiers (they are output in single quotes unless they are lower_words).

Tip: Use the -XOverloadedStrings compiler flag if you don't want to have to type AtomicWord to construct an AtomicWord

Constructors

AtomicWord String 

newtype V Source

Variable names

Constructors

V String 

Fixed-point style decorated formulae and terms

class Pointed a b | b -> a whereSource

This class is used in several utility functions involving F and T.

Conceptually point should be of type a -> m a, but we need the extra flexibility to make restricted monads like Set instances.

Note: We have instance (Monad m) => Pointed a (m a), but Haddock currently doesn't display this.

Methods

point :: a -> bSource

Instances

Monad m => Pointed a (m a) 

class Copointed a b | b -> a whereSource

This class is used in several utility functions involving F and T.

Conceptually copoint should be of type w a -> a, but let's keep the extra flexibility.

Methods

copoint :: b -> aSource

Instances

Utility functions

unwrapF :: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t))) => F t -> Formula0 (T t) (F t)Source

unwrapT :: Copointed (Term0 (T t)) (t (Term0 (T t))) => T t -> Term0 (T t)Source

foldFormula0 :: (f -> r) -> (Quant -> [V] -> f -> r) -> (f -> BinOp -> f -> r) -> (t -> InfixPred -> t -> r) -> (AtomicWord -> [t] -> r) -> Formula0 t f -> rSource

foldTerm0 :: (String -> r) -> (Double -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> rSource

foldFSource

Arguments

:: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t))) 
=> (F t -> r)

Handle negation

-> (Quant -> [V] -> F t -> r)

Handle quantification

-> (F t -> BinOp -> F t -> r)

Handle binary op

-> (T t -> InfixPred -> T t -> r)

Handle equality/inequality

-> (AtomicWord -> [T t] -> r)

Handle predicate symbol application

-> F t -> r

Handle formula

Eliminate formulae

foldTSource

Arguments

:: Copointed (Term0 (T t)) (t (Term0 (T t))) 
=> (String -> r)

Handle string literal

-> (Double -> r)

Handle number literal

-> (V -> r)

Handle variable

-> (AtomicWord -> [T t] -> r)

Handle function symbol application

-> T t -> r

Handle term

Eliminate terms