Copyright  (c) Evgenii Kotelnikov 20192021 

License  GPL3 
Maintainer  evgeny.kotelnikov@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Data structures that represent formulas and theorems in firstorder logic, and smart constructors for them.
Synopsis
 type Var = Integer
 newtype FunctionSymbol = FunctionSymbol Text
 data Term
 newtype PredicateSymbol = PredicateSymbol Text
 data Literal
 data Sign
 data Signed e = Signed {}
 sign :: Sign > Signed e > Signed e
 newtype Clause = Literals {
 getLiterals :: [Signed Literal]
 newtype Clauses = Clauses {
 getClauses :: [Clause]
 data Connective
 = And
  Or
  Implies
  Equivalent
  Xor
 isAssociative :: Connective > Bool
 data Quantifier
 data Formula
 data LogicalExpression
 data Theorem = Theorem {
 axioms :: [Formula]
 conjecture :: Formula
 type Function = [Term] > Term
 type Constant = Term
 type UnaryFunction = Term > Term
 type BinaryFunction = Term > Term > Term
 type TernaryFunction = Term > Term > Term > Term
 pattern Constant :: FunctionSymbol > Constant
 pattern UnaryFunction :: FunctionSymbol > UnaryFunction
 pattern BinaryFunction :: FunctionSymbol > BinaryFunction
 pattern TernaryFunction :: FunctionSymbol > TernaryFunction
 type Predicate = [Term] > Formula
 type Proposition = Formula
 type UnaryPredicate = Term > Formula
 type BinaryPredicate = Term > Term > Formula
 type TernaryPredicate = Term > Term > Term > Formula
 pattern Proposition :: PredicateSymbol > Proposition
 pattern UnaryPredicate :: PredicateSymbol > UnaryPredicate
 pattern BinaryPredicate :: PredicateSymbol > BinaryPredicate
 pattern TernaryPredicate :: PredicateSymbol > TernaryPredicate
 pattern TautologyLiteral :: Signed Literal
 pattern FalsityLiteral :: Signed Literal
 pattern EmptyClause :: Clause
 pattern UnitClause :: Signed Literal > Clause
 pattern TautologyClause :: Clause
 pattern NoClauses :: Clauses
 pattern SingleClause :: Clause > Clauses
 pattern Tautology :: Formula
 pattern Falsity :: Formula
 pattern Claim :: Formula > Theorem
 data AlphaT m a
 evalAlphaT :: Monad m => AlphaT m a > m a
 type Alpha a = AlphaT Identity a
 evalAlpha :: Alpha a > a
 lookup :: Monad m => Var > AlphaT m (Maybe Var)
 scope :: Monad m => AlphaT m [Var]
 enter :: Monad m => Var > Var > AlphaT m a > AlphaT m a
 share :: Monad m => Var > Var > AlphaT m ()
 class Monad m => MonadAlpha m where
 signed :: Sign > Literal > Signed Literal
 unitClause :: Signed Literal > Clause
 clause :: Foldable f => f (Signed Literal) > Clause
 singleClause :: Clause > Clauses
 clauses :: Foldable f => f Clause > Clauses
 (===) :: Term > Term > Formula
 (=/=) :: Term > Term > Formula
 neg :: Formula > Formula
 (\/) :: Formula > Formula > Formula
 (/\) :: Formula > Formula > Formula
 (==>) :: Formula > Formula > Formula
 (<=>) :: Formula > Formula > Formula
 (<~>) :: Formula > Formula > Formula
 class Binder b where
 quantified :: Quantifier > b > Formula
 forall :: Binder b => b > Formula
 exists :: Binder b => b > Formula
 () :: Foldable f => f Formula > Formula > Theorem
 newtype Conjunction = Conjunction {}
 conjunction :: Foldable f => f Formula > Formula
 newtype Disjunction = Disjunction {}
 disjunction :: Foldable f => f Formula > Formula
 newtype Equivalence = Equivalence {}
 equivalence :: Foldable f => f Formula > Formula
 newtype Inequivalence = Inequivalence {}
 inequivalence :: Foldable f => f Formula > Formula
 flattenConjunction :: Foldable f => f Formula > [Formula]
 flattenDisjunction :: Foldable f => f Formula > [Formula]
 class Simplify a where
 simplify :: a > a
 class FirstOrder e where
 closed :: Formula > Bool
 close :: Formula > Formula
 unprefix :: Formula > Formula
 liftSignedLiteral :: Signed Literal > Formula
 unliftSignedLiteral :: Formula > Maybe (Signed Literal)
 liftClause :: Clause > Formula
 unliftClause :: Formula > Maybe Clause
 liftContradiction :: Contradiction f > Inference f
 unliftContradiction :: Inference f > Maybe (Contradiction f)
 liftRefutation :: Ord f => f > Refutation f > Derivation f
 unliftRefutation :: Derivation f > Maybe (Refutation f)
 data Rule f
 = Axiom
  Conjecture
  NegatedConjecture f
  Flattening f
  Skolemisation f
  EnnfTransformation f
  NnfTransformation f
  Clausification f
  TrivialInequality f
  Superposition f f
  Resolution f f
  Paramodulation f f
  SubsumptionResolution f f
  ForwardDemodulation f f
  BackwardDemodulation f f
  AxiomOfChoice
  Unknown [f]
  Other RuleName [f]
 newtype RuleName = RuleName {
 unRuleName :: Text
 ruleName :: Rule f > RuleName
 data Inference f = Inference {}
 antecedents :: Inference f > [f]
 newtype Contradiction f = Contradiction (Rule f)
 data Sequent f = Sequent f (Inference f)
 newtype Derivation f = Derivation (Map f (Inference f))
 addSequent :: Ord f => Derivation f > Sequent f > Derivation f
 breadthFirst :: Ord f => Derivation f > [Sequent f]
 labeling :: Ord f => [Sequent f] > Map f LogicalExpression
 data Refutation f = Refutation (Derivation f) (Contradiction f)
 data Solution
Firstorder logic
newtype FunctionSymbol Source #
The type of function symbols in firstorder formulas.
Instances
The term in firstorder logic.
Variable Var  A quantified variable. 
Function FunctionSymbol [Term]  Application of a function symbol. The empty list of arguments represents a constant. 
Instances
Eq Term Source #  
Ord Term Source #  
Show Term Source #  
IsString Term Source #  
Defined in ATP.FirstOrder.Core fromString :: String > Term #  
Pretty Term Source #  
Defined in ATP.Pretty.FOL  
FirstOrder Term Source #  
Defined in ATP.FirstOrder.Occurrence vars :: Term > Set Var Source # free :: Term > Set Var Source # bound :: Term > Set Var Source # occursIn :: Var > Term > Bool Source # freeIn :: Var > Term > Bool Source # boundIn :: Var > Term > Bool Source # ground :: Term > Bool Source # (~=) :: Term > Term > Bool Source # (?=) :: Term > Term > Alpha Bool Source # alpha :: forall (m :: Type > Type). MonadAlpha m => Term > AlphaT m Term Source #  
Binder b => Binder (Term > b) Source #  The recursive instance for polyvariadic bindings of quantified variables. This is a generalized version of https://emilaxelsson.github.io/documents/axelsson2013using.pdf. 
Defined in ATP.FirstOrder.Smart quantified :: Quantifier > (Term > b) > Formula Source # 
newtype PredicateSymbol Source #
The type of predicate symbols in firstorder formulas.
Instances
The literal in firstorder logic.
Propositional Bool  A logical constant  tautology or falsum. 
Predicate PredicateSymbol [Term]  Application of a predicate symbol. The empty list of arguments represents a boolean constant. 
Equality Term Term  Equality between terms. 
Instances
Eq Literal Source #  
Ord Literal Source #  
Show Literal Source #  
IsString Literal Source #  
Defined in ATP.FirstOrder.Core fromString :: String > Literal #  
Pretty Literal Source #  
Defined in ATP.Pretty.FOL  
FirstOrder Literal Source #  
Defined in ATP.FirstOrder.Occurrence vars :: Literal > Set Var Source # free :: Literal > Set Var Source # bound :: Literal > Set Var Source # occursIn :: Var > Literal > Bool Source # freeIn :: Var > Literal > Bool Source # boundIn :: Var > Literal > Bool Source # ground :: Literal > Bool Source # (~=) :: Literal > Literal > Bool Source # (?=) :: Literal > Literal > Alpha Bool Source # alpha :: forall (m :: Type > Type). MonadAlpha m => Literal > AlphaT m Literal Source #  
Pretty (Signed Literal) Source #  
The sign of a logical expression is either positive or negative.
A signed expression is that annotated with a Sign
.
Instances
The firstorder clause  an implicitly universallyquantified disjunction of positive or negative literals, represented as a list of signed literals. The empty clause is logically equivalent to falsum.
Literals  

Instances
Eq Clause Source #  
Ord Clause Source #  
Show Clause Source #  
IsString Clause Source #  
Defined in ATP.FirstOrder.Core fromString :: String > Clause #  
Semigroup Clause Source #  
Monoid Clause Source #  
Pretty Clause Source #  
Defined in ATP.Pretty.FOL  
FirstOrder Clause Source #  
Defined in ATP.FirstOrder.Occurrence vars :: Clause > Set Var Source # free :: Clause > Set Var Source # bound :: Clause > Set Var Source # occursIn :: Var > Clause > Bool Source # freeIn :: Var > Clause > Bool Source # boundIn :: Var > Clause > Bool Source # ground :: Clause > Bool Source # (~=) :: Clause > Clause > Bool Source # (?=) :: Clause > Clause > Alpha Bool Source # alpha :: forall (m :: Type > Type). MonadAlpha m => Clause > AlphaT m Clause Source #  
Simplify Clause Source #  Simplify the given clause by replacing the

A clause set is zero or more firstorder clauses. The empty clause set is logically equivalent to tautology.
Clauses  

Instances
Eq Clauses Source #  
Ord Clauses Source #  
Show Clauses Source #  
Semigroup Clauses Source #  
Monoid Clauses Source #  
Pretty Clauses Source #  
Defined in ATP.Pretty.FOL  
Simplify Clauses Source #  Simplify the given clause set by replacing the

data Connective Source #
The binary logical connective.
And  Conjunction. 
Or  Disjunction. 
Implies  Implication. 
Equivalent  Equivalence. 
Xor  Exclusive or. 
Instances
isAssociative :: Connective > Bool Source #
Associativity of a given binary logical connective.
>>>
isAssociative Implies
False
>>>
isAssociative And
True
data Quantifier Source #
The quantifier in firstorder logic.
Instances
The formula in firstorder logic.
Atomic Literal  
Negate Formula  
Connected Connective Formula Formula  
Quantified Quantifier Var Formula 
Instances
Eq Formula Source #  
Ord Formula Source #  
Show Formula Source #  
IsString Formula Source #  
Defined in ATP.FirstOrder.Core fromString :: String > Formula #  
Pretty Formula Source #  
Defined in ATP.Pretty.FOL  
FirstOrder Formula Source #  
Defined in ATP.FirstOrder.Occurrence vars :: Formula > Set Var Source # free :: Formula > Set Var Source # bound :: Formula > Set Var Source # occursIn :: Var > Formula > Bool Source # freeIn :: Var > Formula > Bool Source # boundIn :: Var > Formula > Bool Source # ground :: Formula > Bool Source # (~=) :: Formula > Formula > Bool Source # (?=) :: Formula > Formula > Alpha Bool Source # alpha :: forall (m :: Type > Type). MonadAlpha m => Formula > AlphaT m Formula Source #  
Binder Formula Source #  The degenerate instance  no variable is bound. 
Defined in ATP.FirstOrder.Smart quantified :: Quantifier > Formula > Formula Source #  
Simplify Formula Source #  Simplify the given formula by replacing each of its constructors with corresponding smart constructors. The effects of simplification are the following.
Any formula built only using smart constructors is simplified by construction.

Binder (Var, Formula) Source #  The trivial instance  binder of the varible with the given name. 
Defined in ATP.FirstOrder.Smart quantified :: Quantifier > (Var, Formula) > Formula Source # 
data LogicalExpression Source #
A logical expression is either a clause or a formula.
Instances
A theorem is zero or more axioms and a conjecture.
Theorem  

Syntactic sugar
Instances, type synonyms and pattern synonyms for syntactic convenience.
type Function = [Term] > Term Source #
The type of a function symbol  a mapping from zero or more terms to a term.
type UnaryFunction = Term > Term Source #
The type of a function symbol with one argument.
type BinaryFunction = Term > Term > Term Source #
The type of a function symbol with two arguments.
type TernaryFunction = Term > Term > Term > Term Source #
The type of a function symbol with three arguments.
pattern Constant :: FunctionSymbol > Constant Source #
Build a proposition from a predicate symbol.
pattern UnaryFunction :: FunctionSymbol > UnaryFunction Source #
Build a unary function from a function symbol.
pattern BinaryFunction :: FunctionSymbol > BinaryFunction Source #
Build a binary function from a function symbol.
pattern TernaryFunction :: FunctionSymbol > TernaryFunction Source #
Build a ternary function from a function symbol.
type Predicate = [Term] > Formula Source #
The type of a predicate symbol  a mapping from zero or more terms to a formula.
type Proposition = Formula Source #
The type of a proposition.
type UnaryPredicate = Term > Formula Source #
The type of a predicate symbol with one argument.
type BinaryPredicate = Term > Term > Formula Source #
The type of a predicate symbol with two arguments.
type TernaryPredicate = Term > Term > Term > Formula Source #
The type of a function symbol with three arguments.
pattern Proposition :: PredicateSymbol > Proposition Source #
Build a proposition from a predicate symbol.
pattern UnaryPredicate :: PredicateSymbol > UnaryPredicate Source #
Build a unary predicate from a predicate symbol.
pattern BinaryPredicate :: PredicateSymbol > BinaryPredicate Source #
Build a binary predicate from a predicate symbol.
pattern TernaryPredicate :: PredicateSymbol > TernaryPredicate Source #
Build a ternary predicate from a predicate symbol.
pattern TautologyLiteral :: Signed Literal Source #
The positive tautology literal.
pattern FalsityLiteral :: Signed Literal Source #
The positive falsity literal.
pattern EmptyClause :: Clause Source #
The empty clause.
EmptyClause
is semantically (but not syntactically) equivalent to Falsity
.
pattern TautologyClause :: Clause Source #
A unit clause with a single positive tautology literal.
TautologyClause
is semantically (but not syntactically) equivalent to
Tautology
.
pattern SingleClause :: Clause > Clauses Source #
The set of clauses with a single clause in it.
pattern Falsity :: Formula Source #
The logical false.
Falsity
is semantically (but not syntactically) equivalent to EmptyClause
.
pattern Claim :: Formula > Theorem Source #
A logical claim is a conjecture entailed by the empty set of axioms.
The monad transformer that adds to the given monad m
the ability to track
a renaming of free and bound variables in a firstorder expression.
evalAlphaT :: Monad m => AlphaT m a > m a Source #
Evaluate an alpha computation and return the final value, discarding the global scope.
type Alpha a = AlphaT Identity a Source #
The alpha monad parametrized by the type a
of the return value.
evalAlpha :: Alpha a > a Source #
Evaluate an Alpha
computation and return the final value,
discarding the final variable renaming.
lookup :: Monad m => Var > AlphaT m (Maybe Var) Source #
Lookup a variable, first in the stack of bound variables, then in the global scope.
scope :: Monad m => AlphaT m [Var] Source #
Read the set of free and bound variables of the given AlphaT
computation.
enter :: Monad m => Var > Var > AlphaT m a > AlphaT m a Source #
Run a computation inside AlphaT
with the variable renaming.
share :: Monad m => Var > Var > AlphaT m () Source #
Update the global scope with a variable renaming.
class Monad m => MonadAlpha m where Source #
A helper monad for computations on free and bound occurrences of variables.
Smart constructors
clause :: Foldable f => f (Signed Literal) > Clause Source #
A smart contructor for a clause.
clause
eliminates negated boolean constants, falsums and redundant tautologies.
singleClause :: Clause > Clauses Source #
A smart constructor for a set of clauses with a single clause in it.
clauses :: Foldable f => f Clause > Clauses Source #
A smart constructor for the set of clauses.
clauses
eliminates negated boolean constants, falsums and redundant tautologies.
(==>) :: Formula > Formula > Formula infix 5 Source #
A smart constructor for the Implies
connective.
(<=>) :: Formula > Formula > Formula infixl 5 Source #
A smart constructor for the Equivalent
connective.
(<=>
) has the following properties.
Associativity
(f <=> g) <=> h == f <=> (g <=> h)
Left identity
Tautology <=> g == g
Right identity
f <=> Tautology == f
A class of binders for quantified variables.
This class and its instances provides machinery for using polyvariadic functions as higherorder abstract syntax for bindings of quantified variables.
eq = binaryPredicate "eq"
>>>
quantified Forall $ \x > x `eq` x
Quantified Forall 1 (Atomic (Predicate "eq" [Variable 1,Variable 1]))
>>>
quantified Forall $ \x y > x `eq` y ==> y `eq` x
Quantified Forall 2 (Quantified Forall 1 (Connected Implies (Atomic (Predicate "eq" [Variable 2,Variable 1])) (Atomic (Predicate "eq" [Variable 1,Variable 2]))))
quantified :: Quantifier > b > Formula Source #
A smart constructor for quantified formulas.
Instances
Binder Formula Source #  The degenerate instance  no variable is bound. 
Defined in ATP.FirstOrder.Smart quantified :: Quantifier > Formula > Formula Source #  
Binder b => Binder (Term > b) Source #  The recursive instance for polyvariadic bindings of quantified variables. This is a generalized version of https://emilaxelsson.github.io/documents/axelsson2013using.pdf. 
Defined in ATP.FirstOrder.Smart quantified :: Quantifier > (Term > b) > Formula Source #  
Binder (Var, Formula) Source #  The trivial instance  binder of the varible with the given name. 
Defined in ATP.FirstOrder.Smart quantified :: Quantifier > (Var, Formula) > Formula Source # 
forall :: Binder b => b > Formula Source #
A smart constructor for universally quantified formulas. Provides a polyvariadic higherorder abstract syntax for the bindings of universally quantified variables.
exists :: Binder b => b > Formula Source #
A smart constructor for existentially quantified formulas. Provides a polyvariadic higherorder abstract syntax for the bindings of existentially quantified variables.
Monoids
newtype Conjunction Source #
Instances
conjunction :: Foldable f => f Formula > Formula Source #
Build the conjunction of formulas in a list.
newtype Disjunction Source #
Instances
disjunction :: Foldable f => f Formula > Formula Source #
Build the disjunction of formulas in a list.
newtype Equivalence Source #
Instances
equivalence :: Foldable f => f Formula > Formula Source #
Build the equivalence of formulas in a list.
newtype Inequivalence Source #
Instances
inequivalence :: Foldable f => f Formula > Formula Source #
Build the inequivalence of formulas in a list.
Miscellaneous
flattenConjunction :: Foldable f => f Formula > [Formula] Source #
Remove redundant boolean constants from a list of conjuncted formulas.
>>>
flattenConjunction []
[]
>>>
flattenConjunction [Tautology]
[]
>>>
flattenConjunction [Falsity]
[Atomic (Propositional False)]
>>>
flattenConjunction ["p", Tautology]
[Atomic (Predicate (PredicateSymbol "p") [])]
>>>
flattenConjunction ["p", Falsity, "q"]
[Atomic (Propositional False)]
flattenDisjunction :: Foldable f => f Formula > [Formula] Source #
Remove redundant boolean constants from a list of disjuncted formulas.
>>>
flattenDisjunction []
[]
>>>
flattenDisjunction [Tautology]
[Atomic (Propositional True)]
>>>
flattenDisjunction [Falsity]
[]
>>>
flattenDisjunction ["p", Tautology, "q"]
[Atomic (Propositional True)]
>>>
flattenDisjunction ["p", Falsity]
[Atomic (Predicate (PredicateSymbol "p") [])]
Simplification
class Simplify a where Source #
A class of firstorder expressions that simplify
syntactically shrinks
while preserving their evaluation.
Instances
Simplify Theorem Source #  Simplify the given theorem by flattening the conjunction of its premises and its conjecture. 
Simplify LogicalExpression Source #  Simplify the given formula by replacing each of its constructors with corresponding smart constructors. 
Defined in ATP.FirstOrder.Simplification  
Simplify Formula Source #  Simplify the given formula by replacing each of its constructors with corresponding smart constructors. The effects of simplification are the following.
Any formula built only using smart constructors is simplified by construction.

Simplify Clauses Source #  Simplify the given clause set by replacing the

Simplify Clause Source #  Simplify the given clause by replacing the

Occurrence
class FirstOrder e where Source #
A class of firstorder expressions, i.e. expressions that might contain
variables.
s, Formula
s and Literal
s are firstorder expressions.Term
A variable can occur both as free and bound, therefore
and free
e
are not necessarily disjoint and
bound
ev
and freeIn
ev
are not necessarily musually exclusive.boundIn
e
, vars
and free
are connected by the following property.bound
free e <> bound e == vars e
, occursIn
and freeIn
are connected by the following property.boundIn
v `freeIn` e  v `boundIn` e == v `occursIn` e
The set of all variables that occur anywhere in the given expression.
The set of variables that occur freely in the given expression, i.e. are not bound by any quantifier inside the expression.
bound :: e > Set Var Source #
The set of variables that occur bound in the given expression, i.e. are bound by a quantifier inside the expression.
occursIn :: Var > e > Bool Source #
Check whether the given variable occurs anywhere in the given expression.
freeIn :: Var > e > Bool Source #
Check whether the given variable occurs freely anywhere in the given expression.
boundIn :: Var > e > Bool Source #
Check whether the given variable occurs bound anywhere in the given expression.
Check whether the given expression is ground, i.e. does not contain any variables.
Note that ground formula is sometimes understood as formula that does
not contain any free variables. In this library such formulas are called
.closed
(~=) :: e > e > Bool infix 5 Source #
Check whether two given expressions are alphaequivalent, that is equivalent up to renaming of variables.
(~=)
is an equivalence relation.
Symmetry
e ~= e
Reflexivity
a ~= b == b ~= a
Transitivity
a ~= b && b ~= c ==> a ~= c
(?=) :: e > e > Alpha Bool Source #
A helper function calculating alphaequivalence using the Alpha
monad stack.
alpha :: MonadAlpha m => e > AlphaT m e Source #
Instances
closed :: Formula > Bool Source #
Check whether the given formula is closed, i.e. does not contain any free variables.
unprefix :: Formula > Formula Source #
Remove the toplevel quantifiers.
>>>
unprefix (Quantified Forall 1 (Quantified Exists 2 (Atomic (Equality (Variable 1) (Variable 2)))))
Atomic (Equality (Variable 1) (Variable 2))
Conversions
Formulas
liftSignedLiteral :: Signed Literal > Formula Source #
Convert a signed literal to a (negated) atomic formula.
unliftSignedLiteral :: Formula > Maybe (Signed Literal) Source #
Try to convert a firstorder formula f to a signed literal. This function succeeds if f is a (negated) atomic formula.
liftClause :: Clause > Formula Source #
Convert a clause to a full firstorder formula.
unliftClause :: Formula > Maybe Clause Source #
Try to convert a firstorder formula f to a clause. This function succeeds if f is a tree of disjunctions of (negated) atomic formula.
Proofs
liftContradiction :: Contradiction f > Inference f Source #
Convert a contradiction to an inference.
unliftContradiction :: Inference f > Maybe (Contradiction f) Source #
Try to convert an inference to a contradiction.
liftRefutation :: Ord f => f > Refutation f > Derivation f Source #
Convert a refutation to a derivation.
unliftRefutation :: Derivation f > Maybe (Refutation f) Source #
Try to convert a derivation to a refutation. This function succeds if the derivation has exactly one inference resulting in contradiction.
Proofs
The inference rule.
Axiom  
Conjecture  
NegatedConjecture f  
Flattening f  
Skolemisation f  
EnnfTransformation f  
NnfTransformation f  
Clausification f  
TrivialInequality f  
Superposition f f  
Resolution f f  
Paramodulation f f  
SubsumptionResolution f f  
ForwardDemodulation f f  
BackwardDemodulation f f  
AxiomOfChoice  
Unknown [f]  
Other RuleName [f] 
Instances
Functor Rule Source #  
Foldable Rule Source #  
Defined in ATP.FirstOrder.Derivation fold :: Monoid m => Rule m > m # foldMap :: Monoid m => (a > m) > Rule a > m # foldMap' :: Monoid m => (a > m) > Rule a > m # foldr :: (a > b > b) > b > Rule a > b # foldr' :: (a > b > b) > b > Rule a > b # foldl :: (b > a > b) > b > Rule a > b # foldl' :: (b > a > b) > b > Rule a > b # foldr1 :: (a > a > a) > Rule a > a # foldl1 :: (a > a > a) > Rule a > a # elem :: Eq a => a > Rule a > Bool # maximum :: Ord a => Rule a > a #  
Traversable Rule Source #  
Eq f => Eq (Rule f) Source #  
Ord f => Ord (Rule f) Source #  
Show f => Show (Rule f) Source #  
Pretty l => Pretty (Rule l) Source #  
Defined in ATP.Pretty.FOL 
The name of an inference rule.
ruleName :: Rule f > RuleName Source #
The name of the given inference rule.
>>>
unRuleName (ruleName AxiomOfChoice)
"axiom of choice"
A logical inference is an expression of the form
A_1 ... A_n  R, C
where each of A_1
, ... A_n
(called the antecedents
), and C
(called the consequent
) are formulas and R
is an inference Rule
.
Instances
Functor Inference Source #  
Foldable Inference Source #  
Defined in ATP.FirstOrder.Derivation fold :: Monoid m => Inference m > m # foldMap :: Monoid m => (a > m) > Inference a > m # foldMap' :: Monoid m => (a > m) > Inference a > m # foldr :: (a > b > b) > b > Inference a > b # foldr' :: (a > b > b) > b > Inference a > b # foldl :: (b > a > b) > b > Inference a > b # foldl' :: (b > a > b) > b > Inference a > b # foldr1 :: (a > a > a) > Inference a > a # foldl1 :: (a > a > a) > Inference a > a # toList :: Inference a > [a] # length :: Inference a > Int # elem :: Eq a => a > Inference a > Bool # maximum :: Ord a => Inference a > a # minimum :: Ord a => Inference a > a #  
Traversable Inference Source #  
Defined in ATP.FirstOrder.Derivation  
Eq f => Eq (Inference f) Source #  
Ord f => Ord (Inference f) Source #  
Defined in ATP.FirstOrder.Derivation  
Show f => Show (Inference f) Source #  
Pretty l => Pretty (Inference l) Source #  
Defined in ATP.Pretty.FOL 
antecedents :: Inference f > [f] Source #
The antecedents of an inference.
newtype Contradiction f Source #
Contradiction is a special case of an inference that has the logical falsum as the consequent.
Contradiction (Rule f) 
Instances
A sequent is a logical inference, annotated with a label. Linked sequents form derivations.
Instances
Functor Sequent Source #  
Foldable Sequent Source #  
Defined in ATP.FirstOrder.Derivation fold :: Monoid m => Sequent m > m # foldMap :: Monoid m => (a > m) > Sequent a > m # foldMap' :: Monoid m => (a > m) > Sequent a > m # foldr :: (a > b > b) > b > Sequent a > b # foldr' :: (a > b > b) > b > Sequent a > b # foldl :: (b > a > b) > b > Sequent a > b # foldl' :: (b > a > b) > b > Sequent a > b # foldr1 :: (a > a > a) > Sequent a > a # foldl1 :: (a > a > a) > Sequent a > a # elem :: Eq a => a > Sequent a > Bool # maximum :: Ord a => Sequent a > a # minimum :: Ord a => Sequent a > a #  
Traversable Sequent Source #  
Eq f => Eq (Sequent f) Source #  
Ord f => Ord (Sequent f) Source #  
Defined in ATP.FirstOrder.Derivation  
Show f => Show (Sequent f) Source #  
Pretty l => Pretty (Sequent l) Source #  
Defined in ATP.Pretty.FOL 
newtype Derivation f Source #
A derivation is a directed asyclic graph of logical inferences.
In this graph nodes are formulas and edges are inference rules.
The type parameter f
is used to label and index the nodes.
Derivation (Map f (Inference f)) 
Instances
addSequent :: Ord f => Derivation f > Sequent f > Derivation f Source #
Attach a sequent to a derivation.
breadthFirst :: Ord f => Derivation f > [Sequent f] Source #
Traverse the given derivation breadthfirst and produce a list of sequents.
labeling :: Ord f => [Sequent f] > Map f LogicalExpression Source #
Construct a mapping between inference labels and their correspondent formulas.
data Refutation f Source #
A refutation is a special case of a derivation that results in a contradiction. A successful proof produces by an automated theorem prover is a proof by refutation.
Refutation (Derivation f) (Contradiction f) 
Instances
Eq f => Eq (Refutation f) Source #  
Defined in ATP.FirstOrder.Derivation (==) :: Refutation f > Refutation f > Bool # (/=) :: Refutation f > Refutation f > Bool #  
Ord f => Ord (Refutation f) Source #  
Defined in ATP.FirstOrder.Derivation compare :: Refutation f > Refutation f > Ordering # (<) :: Refutation f > Refutation f > Bool # (<=) :: Refutation f > Refutation f > Bool # (>) :: Refutation f > Refutation f > Bool # (>=) :: Refutation f > Refutation f > Bool # max :: Refutation f > Refutation f > Refutation f # min :: Refutation f > Refutation f > Refutation f #  
Show f => Show (Refutation f) Source #  
Defined in ATP.FirstOrder.Derivation showsPrec :: Int > Refutation f > ShowS # show :: Refutation f > String # showList :: [Refutation f] > ShowS #  
(Ord l, Pretty l) => Pretty (Refutation l) Source #  
Defined in ATP.Pretty.FOL pretty :: Refutation l > Doc # prettyList :: [Refutation l] > Doc # 
The solution produced by an automated firstorder theorem prover.
Saturation (Derivation Integer)  A theorem can be disproven if the prover constructs a saturated set of firstorder clauses. 
Proof (Refutation Integer)  A theorem can be proven if the prover derives contradiction (the empty clause) from the set of axioms and the negated conjecture. 