ATP.FOL

Data structures that represent formulas and theorems in first-order logic, and smart constructors for them.

First-order logic

type Var = Integer

The type of variables in first-order formulas.

newtype FunctionSymbol

The type of function symbols in first-order formulas.

Constructors

FunctionSymbol Text

Instances

Eq FunctionSymbol

Defined in ATP.FirstOrder.Core

Methods

(==) :: FunctionSymbol -> FunctionSymbol -> Bool

(/=) :: FunctionSymbol -> FunctionSymbol -> Bool

Ord FunctionSymbol

Defined in ATP.FirstOrder.Core

Methods

compare :: FunctionSymbol -> FunctionSymbol -> Ordering

(<) :: FunctionSymbol -> FunctionSymbol -> Bool

(<=) :: FunctionSymbol -> FunctionSymbol -> Bool

(>) :: FunctionSymbol -> FunctionSymbol -> Bool

(>=) :: FunctionSymbol -> FunctionSymbol -> Bool

max :: FunctionSymbol -> FunctionSymbol -> FunctionSymbol

min :: FunctionSymbol -> FunctionSymbol -> FunctionSymbol

Show FunctionSymbol

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> FunctionSymbol -> ShowS

show :: FunctionSymbol -> String

showList :: [FunctionSymbol] -> ShowS

IsString FunctionSymbol

Defined in ATP.FirstOrder.Core

Methods

fromString :: String -> FunctionSymbol

Pretty FunctionSymbol

Defined in ATP.Pretty.FOL

Methods

pretty :: FunctionSymbol -> Doc

prettyList :: [FunctionSymbol] -> Doc

data Term

The term in first-order logic.

Constructors

Variable Var

A quantified variable.

Function FunctionSymbol [Term]

Application of a function symbol. The empty list of arguments represents a constant.

Instances

Eq Term

Defined in ATP.FirstOrder.Core

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Ord Term

Defined in ATP.FirstOrder.Core

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Show Term

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

IsString Term

Defined in ATP.FirstOrder.Core

Methods

fromString :: String -> Term

Pretty Term

Defined in ATP.Pretty.FOL

Methods

pretty :: Term -> Doc

prettyList :: [Term] -> Doc

FirstOrder Term

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Term -> Set Var

free :: Term -> Set Var

bound :: Term -> Set Var

occursIn :: Var -> Term -> Bool

freeIn :: Var -> Term -> Bool

boundIn :: Var -> Term -> Bool

ground :: Term -> Bool

(~=) :: Term -> Term -> Bool

(?=) :: Term -> Term -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Term -> AlphaT m Term

Binder b => Binder (Term -> b)

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

Methods

quantified :: Quantifier -> (Term -> b) -> Formula

newtype PredicateSymbol

The type of predicate symbols in first-order formulas.

Constructors

PredicateSymbol Text

Instances

Eq PredicateSymbol

Defined in ATP.FirstOrder.Core

Methods

(==) :: PredicateSymbol -> PredicateSymbol -> Bool

(/=) :: PredicateSymbol -> PredicateSymbol -> Bool

Ord PredicateSymbol

Defined in ATP.FirstOrder.Core

Methods

compare :: PredicateSymbol -> PredicateSymbol -> Ordering

(<) :: PredicateSymbol -> PredicateSymbol -> Bool

(<=) :: PredicateSymbol -> PredicateSymbol -> Bool

(>) :: PredicateSymbol -> PredicateSymbol -> Bool

(>=) :: PredicateSymbol -> PredicateSymbol -> Bool

max :: PredicateSymbol -> PredicateSymbol -> PredicateSymbol

min :: PredicateSymbol -> PredicateSymbol -> PredicateSymbol

Show PredicateSymbol

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> PredicateSymbol -> ShowS

show :: PredicateSymbol -> String

showList :: [PredicateSymbol] -> ShowS

IsString PredicateSymbol

Defined in ATP.FirstOrder.Core

Methods

fromString :: String -> PredicateSymbol

Pretty PredicateSymbol

Defined in ATP.Pretty.FOL

Methods

pretty :: PredicateSymbol -> Doc

prettyList :: [PredicateSymbol] -> Doc

data Literal

The literal in first-order logic.

Constructors

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

Defined in ATP.FirstOrder.Core

Methods

(==) :: Literal -> Literal -> Bool

(/=) :: Literal -> Literal -> Bool

Ord Literal

Defined in ATP.FirstOrder.Core

Methods

compare :: Literal -> Literal -> Ordering

(<) :: Literal -> Literal -> Bool

(<=) :: Literal -> Literal -> Bool

(>) :: Literal -> Literal -> Bool

(>=) :: Literal -> Literal -> Bool

max :: Literal -> Literal -> Literal

min :: Literal -> Literal -> Literal

Show Literal

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

IsString Literal

Defined in ATP.FirstOrder.Core

Methods

fromString :: String -> Literal

Pretty Literal

Defined in ATP.Pretty.FOL

Methods

pretty :: Literal -> Doc

prettyList :: [Literal] -> Doc

FirstOrder Literal

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Literal -> Set Var

free :: Literal -> Set Var

bound :: Literal -> Set Var

occursIn :: Var -> Literal -> Bool

freeIn :: Var -> Literal -> Bool

boundIn :: Var -> Literal -> Bool

ground :: Literal -> Bool

(~=) :: Literal -> Literal -> Bool

(?=) :: Literal -> Literal -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Literal -> AlphaT m Literal

Pretty (Signed Literal)

Defined in ATP.Pretty.FOL

Methods

pretty :: Signed Literal -> Doc

prettyList :: [Signed Literal] -> Doc

data Sign

The sign of a logical expression is either positive or negative.

Constructors

Positive

Negative

Instances

Bounded Sign

Defined in ATP.FirstOrder.Core

Methods

minBound :: Sign

maxBound :: Sign

Enum Sign

Defined in ATP.FirstOrder.Core

Methods

succ :: Sign -> Sign

pred :: Sign -> Sign

toEnum :: Int -> Sign

fromEnum :: Sign -> Int

enumFrom :: Sign -> [Sign]

enumFromThen :: Sign -> Sign -> [Sign]

enumFromTo :: Sign -> Sign -> [Sign]

enumFromThenTo :: Sign -> Sign -> Sign -> [Sign]

Eq Sign

Defined in ATP.FirstOrder.Core

Methods

(==) :: Sign -> Sign -> Bool

(/=) :: Sign -> Sign -> Bool

Ord Sign

Defined in ATP.FirstOrder.Core

Methods

compare :: Sign -> Sign -> Ordering

(<) :: Sign -> Sign -> Bool

(<=) :: Sign -> Sign -> Bool

(>) :: Sign -> Sign -> Bool

(>=) :: Sign -> Sign -> Bool

max :: Sign -> Sign -> Sign

min :: Sign -> Sign -> Sign

Show Sign

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Sign -> ShowS

show :: Sign -> String

showList :: [Sign] -> ShowS

Semigroup Sign

Defined in ATP.FirstOrder.Core

Methods

(<>) :: Sign -> Sign -> Sign

sconcat :: NonEmpty Sign -> Sign

stimes :: Integral b => b -> Sign -> Sign

Monoid Sign

Defined in ATP.FirstOrder.Core

Methods

mempty :: Sign

mappend :: Sign -> Sign -> Sign

mconcat :: [Sign] -> Sign

data Signed e

A signed expression is that annotated with a Sign.

Constructors

Signed

Fields

• signof :: Sign
• unsign :: e

Instances

Monad Signed

Defined in ATP.FirstOrder.Core

Methods

(>>=) :: Signed a -> (a -> Signed b) -> Signed b

(>>) :: Signed a -> Signed b -> Signed b

return :: a -> Signed a

Functor Signed

Defined in ATP.FirstOrder.Core

Methods

fmap :: (a -> b) -> Signed a -> Signed b

(<$) :: a -> Signed b -> Signed a

Applicative Signed

Defined in ATP.FirstOrder.Core

Methods

pure :: a -> Signed a

(<*>) :: Signed (a -> b) -> Signed a -> Signed b

liftA2 :: (a -> b -> c) -> Signed a -> Signed b -> Signed c

(*>) :: Signed a -> Signed b -> Signed b

(<*) :: Signed a -> Signed b -> Signed a

Foldable Signed

Defined in ATP.FirstOrder.Core

Methods

fold :: Monoid m => Signed m -> m

foldMap :: Monoid m => (a -> m) -> Signed a -> m

foldMap' :: Monoid m => (a -> m) -> Signed a -> m

foldr :: (a -> b -> b) -> b -> Signed a -> b

foldr' :: (a -> b -> b) -> b -> Signed a -> b

foldl :: (b -> a -> b) -> b -> Signed a -> b

foldl' :: (b -> a -> b) -> b -> Signed a -> b

foldr1 :: (a -> a -> a) -> Signed a -> a

foldl1 :: (a -> a -> a) -> Signed a -> a

toList :: Signed a -> [a]

null :: Signed a -> Bool

length :: Signed a -> Int

elem :: Eq a => a -> Signed a -> Bool

maximum :: Ord a => Signed a -> a

minimum :: Ord a => Signed a -> a

sum :: Num a => Signed a -> a

product :: Num a => Signed a -> a

Traversable Signed

Defined in ATP.FirstOrder.Core

Methods

traverse :: Applicative f => (a -> f b) -> Signed a -> f (Signed b)

sequenceA :: Applicative f => Signed (f a) -> f (Signed a)

mapM :: Monad m => (a -> m b) -> Signed a -> m (Signed b)

sequence :: Monad m => Signed (m a) -> m (Signed a)

Eq e => Eq (Signed e)

Defined in ATP.FirstOrder.Core

Methods

(==) :: Signed e -> Signed e -> Bool

(/=) :: Signed e -> Signed e -> Bool

Ord e => Ord (Signed e)

Defined in ATP.FirstOrder.Core

Methods

compare :: Signed e -> Signed e -> Ordering

(<) :: Signed e -> Signed e -> Bool

(<=) :: Signed e -> Signed e -> Bool

(>) :: Signed e -> Signed e -> Bool

(>=) :: Signed e -> Signed e -> Bool

max :: Signed e -> Signed e -> Signed e

min :: Signed e -> Signed e -> Signed e

Show e => Show (Signed e)

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Signed e -> ShowS

show :: Signed e -> String

showList :: [Signed e] -> ShowS

IsString e => IsString (Signed e)

Defined in ATP.FirstOrder.Core

Methods

fromString :: String -> Signed e

Pretty (Signed Literal)

Defined in ATP.Pretty.FOL

Methods

pretty :: Signed Literal -> Doc

prettyList :: [Signed Literal] -> Doc

FirstOrder e => FirstOrder (Signed e)

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Signed e -> Set Var

free :: Signed e -> Set Var

bound :: Signed e -> Set Var

occursIn :: Var -> Signed e -> Bool

freeIn :: Var -> Signed e -> Bool

boundIn :: Var -> Signed e -> Bool

ground :: Signed e -> Bool

(~=) :: Signed e -> Signed e -> Bool

(?=) :: Signed e -> Signed e -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Signed e -> AlphaT m (Signed e)

sign :: Sign -> Signed e -> Signed e

Juxtapose a given signed expression with a given sign.

newtype Clause

The first-order clause - an implicitly universally-quantified disjunction of positive or negative literals, represented as a list of signed literals. The empty clause is logically equivalent to falsum.

Constructors

Literals

Fields

• getLiterals :: [Signed Literal]

Instances

Eq Clause

Defined in ATP.FirstOrder.Core

Methods

(==) :: Clause -> Clause -> Bool

(/=) :: Clause -> Clause -> Bool

Ord Clause

Defined in ATP.FirstOrder.Core

Methods

compare :: Clause -> Clause -> Ordering

(<) :: Clause -> Clause -> Bool

(<=) :: Clause -> Clause -> Bool

(>) :: Clause -> Clause -> Bool

(>=) :: Clause -> Clause -> Bool

max :: Clause -> Clause -> Clause

min :: Clause -> Clause -> Clause

Show Clause

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

IsString Clause

Defined in ATP.FirstOrder.Core

Methods

fromString :: String -> Clause

Semigroup Clause

Defined in ATP.FirstOrder.Core

Methods

(<>) :: Clause -> Clause -> Clause

sconcat :: NonEmpty Clause -> Clause

stimes :: Integral b => b -> Clause -> Clause

Monoid Clause

Defined in ATP.FirstOrder.Core

Methods

mempty :: Clause

mappend :: Clause -> Clause -> Clause

mconcat :: [Clause] -> Clause

Pretty Clause

Defined in ATP.Pretty.FOL

Methods

pretty :: Clause -> Doc

prettyList :: [Clause] -> Doc

FirstOrder Clause

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Clause -> Set Var

free :: Clause -> Set Var

bound :: Clause -> Set Var

occursIn :: Var -> Clause -> Bool

freeIn :: Var -> Clause -> Bool

boundIn :: Var -> Clause -> Bool

ground :: Clause -> Bool

(~=) :: Clause -> Clause -> Bool

(?=) :: Clause -> Clause -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Clause -> AlphaT m Clause

Simplify Clause

Simplify the given clause by replacing the Literals constructor with the smart constructor clause. The effects of simplification are the following.

• simplify c does not contain negative constant literals.
• simplify c does not contain falsum literals.
• simplify c does not contain redundant tautology literals.

>>> simplify (UnitClause (Signed Negative (Propositional True)))
Literals {getLiterals = []}

>>> simplify (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])])
Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}

>>> simplify (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])])
Literals {getLiterals = [Signed {signof = Positive, unsign = Propositional True}]}

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Clause -> Clause

newtype Clauses

A clause set is zero or more first-order clauses. The empty clause set is logically equivalent to tautology.

Constructors

Clauses

Fields

• getClauses :: [Clause]

Instances

Eq Clauses

Defined in ATP.FirstOrder.Core

Methods

(==) :: Clauses -> Clauses -> Bool

(/=) :: Clauses -> Clauses -> Bool

Ord Clauses

Defined in ATP.FirstOrder.Core

Methods

compare :: Clauses -> Clauses -> Ordering

(<) :: Clauses -> Clauses -> Bool

(<=) :: Clauses -> Clauses -> Bool

(>) :: Clauses -> Clauses -> Bool

(>=) :: Clauses -> Clauses -> Bool

max :: Clauses -> Clauses -> Clauses

min :: Clauses -> Clauses -> Clauses

Show Clauses

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Clauses -> ShowS

show :: Clauses -> String

showList :: [Clauses] -> ShowS

Semigroup Clauses

Defined in ATP.FirstOrder.Core

Methods

(<>) :: Clauses -> Clauses -> Clauses

sconcat :: NonEmpty Clauses -> Clauses

stimes :: Integral b => b -> Clauses -> Clauses

Monoid Clauses

Defined in ATP.FirstOrder.Core

Methods

mempty :: Clauses

mappend :: Clauses -> Clauses -> Clauses

mconcat :: [Clauses] -> Clauses

Pretty Clauses

Defined in ATP.Pretty.FOL

Methods

pretty :: Clauses -> Doc

prettyList :: [Clauses] -> Doc

Simplify Clauses

Simplify the given clause set by replacing the Clauses constructor with the smart constructor clauses. The effects of simplification are the following.

• simplify c does not contain negative constant literals.
• simplify c does not contain falsum literals.
• simplify c does not contain tautology literals.
• simplify c does not contain redundant falsum literals.

>>> simplify (SingleClause (UnitClause (Signed Negative (Propositional True))))
Clauses {getClauses = [Literals {getLiterals = []}]}

>>> simplify (SingleClause (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])]))
Clauses {getClauses = [Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}]}

>>> simplify (SingleClause (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])]))
Clauses {getClauses = []}

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Clauses -> Clauses

data Connective

The binary logical connective.

Constructors

And

Conjunction.

Or

Disjunction.

Implies

Implication.

Equivalent

Equivalence.

Xor

Exclusive or.

Instances

Bounded Connective

Defined in ATP.FirstOrder.Core

Methods

minBound :: Connective

maxBound :: Connective

Enum Connective

Defined in ATP.FirstOrder.Core

Methods

succ :: Connective -> Connective

pred :: Connective -> Connective

toEnum :: Int -> Connective

fromEnum :: Connective -> Int

enumFrom :: Connective -> [Connective]

enumFromThen :: Connective -> Connective -> [Connective]

enumFromTo :: Connective -> Connective -> [Connective]

enumFromThenTo :: Connective -> Connective -> Connective -> [Connective]

Eq Connective

Defined in ATP.FirstOrder.Core

Methods

(==) :: Connective -> Connective -> Bool

(/=) :: Connective -> Connective -> Bool

Ord Connective

Defined in ATP.FirstOrder.Core

Methods

compare :: Connective -> Connective -> Ordering

(<) :: Connective -> Connective -> Bool

(<=) :: Connective -> Connective -> Bool

(>) :: Connective -> Connective -> Bool

(>=) :: Connective -> Connective -> Bool

max :: Connective -> Connective -> Connective

min :: Connective -> Connective -> Connective

Show Connective

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Connective -> ShowS

show :: Connective -> String

showList :: [Connective] -> ShowS

Pretty Connective

Defined in ATP.Pretty.FOL

Methods

pretty :: Connective -> Doc

prettyList :: [Connective] -> Doc

isAssociative :: Connective -> Bool

Associativity of a given binary logical connective.

>>> isAssociative Implies
False

>>> isAssociative And
True

data Quantifier

The quantifier in first-order logic.

Constructors

Forall

The universal quantifier.

Exists

The existential quantifier.

Instances

Bounded Quantifier

Defined in ATP.FirstOrder.Core

Methods

minBound :: Quantifier

maxBound :: Quantifier

Enum Quantifier

Defined in ATP.FirstOrder.Core

Methods

succ :: Quantifier -> Quantifier

pred :: Quantifier -> Quantifier

toEnum :: Int -> Quantifier

fromEnum :: Quantifier -> Int

enumFrom :: Quantifier -> [Quantifier]

enumFromThen :: Quantifier -> Quantifier -> [Quantifier]

enumFromTo :: Quantifier -> Quantifier -> [Quantifier]

enumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]

Eq Quantifier

Defined in ATP.FirstOrder.Core

Methods

(==) :: Quantifier -> Quantifier -> Bool

(/=) :: Quantifier -> Quantifier -> Bool

Ord Quantifier

Defined in ATP.FirstOrder.Core

Methods

compare :: Quantifier -> Quantifier -> Ordering

(<) :: Quantifier -> Quantifier -> Bool

(<=) :: Quantifier -> Quantifier -> Bool

(>) :: Quantifier -> Quantifier -> Bool

(>=) :: Quantifier -> Quantifier -> Bool

max :: Quantifier -> Quantifier -> Quantifier

min :: Quantifier -> Quantifier -> Quantifier

Show Quantifier

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Quantifier -> ShowS

show :: Quantifier -> String

showList :: [Quantifier] -> ShowS

Pretty Quantifier

Defined in ATP.Pretty.FOL

Methods

pretty :: Quantifier -> Doc

prettyList :: [Quantifier] -> Doc

data Formula

The formula in first-order logic.

Constructors

Atomic Literal

Negate Formula

Connected Connective Formula Formula

Quantified Quantifier Var Formula

Instances

Eq Formula

Defined in ATP.FirstOrder.Core

Methods

(==) :: Formula -> Formula -> Bool

(/=) :: Formula -> Formula -> Bool

Ord Formula

Defined in ATP.FirstOrder.Core

Methods

compare :: Formula -> Formula -> Ordering

(<) :: Formula -> Formula -> Bool

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

(>) :: Formula -> Formula -> Bool

(>=) :: Formula -> Formula -> Bool

max :: Formula -> Formula -> Formula

min :: Formula -> Formula -> Formula

Show Formula

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Formula -> ShowS

show :: Formula -> String

showList :: [Formula] -> ShowS

IsString Formula

Defined in ATP.FirstOrder.Core

Methods

fromString :: String -> Formula

Pretty Formula

Defined in ATP.Pretty.FOL

Methods

pretty :: Formula -> Doc

prettyList :: [Formula] -> Doc

FirstOrder Formula

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Formula -> Set Var

free :: Formula -> Set Var

bound :: Formula -> Set Var

occursIn :: Var -> Formula -> Bool

freeIn :: Var -> Formula -> Bool

boundIn :: Var -> Formula -> Bool

ground :: Formula -> Bool

(~=) :: Formula -> Formula -> Bool

(?=) :: Formula -> Formula -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Formula -> AlphaT m Formula

Binder Formula

The degenerate instance - no variable is bound.

Defined in ATP.FirstOrder.Smart

Methods

quantified :: Quantifier -> Formula -> Formula

Simplify Formula

Simplify the given formula by replacing each of its constructors with corresponding smart constructors. The effects of simplification are the following.

• simplify f does not contain nested negations.
• simplify f does not contain some of the constant atomic formulas from f.
• All chained applications of any binary connective inside simplify f are right-associative.

Any formula built only using smart constructors is simplified by construction.

>>> simplify (Connected Or tautology (Atomic (Predicate "p" [])))
Atomic (Propositional True)

>>> simplify (Negate (Negate (Atomic (Predicate "p" []))))
Atomic (Predicate "p" [])

>>> simplify (Connected And (Connected And (Atomic (Predicate "p" [])) (Atomic (Predicate "q" []))) (Atomic (Predicate "r" [])))
Connected And (Atomic (Predicate "p" [])) (Connected And (Atomic (Predicate "q" [])) (Atomic (Predicate "r" [])))

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Formula -> Formula

Binder (Var, Formula)

The trivial instance - binder of the varible with the given name.

Defined in ATP.FirstOrder.Smart

Methods

quantified :: Quantifier -> (Var, Formula) -> Formula

data LogicalExpression

A logical expression is either a clause or a formula.

Constructors

Clause Clause

Formula Formula

Instances

Eq LogicalExpression

Defined in ATP.FirstOrder.Core

Methods

(==) :: LogicalExpression -> LogicalExpression -> Bool

(/=) :: LogicalExpression -> LogicalExpression -> Bool

Ord LogicalExpression

Defined in ATP.FirstOrder.Core

Methods

compare :: LogicalExpression -> LogicalExpression -> Ordering

(<) :: LogicalExpression -> LogicalExpression -> Bool

(<=) :: LogicalExpression -> LogicalExpression -> Bool

(>) :: LogicalExpression -> LogicalExpression -> Bool

(>=) :: LogicalExpression -> LogicalExpression -> Bool

max :: LogicalExpression -> LogicalExpression -> LogicalExpression

min :: LogicalExpression -> LogicalExpression -> LogicalExpression

Show LogicalExpression

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> LogicalExpression -> ShowS

show :: LogicalExpression -> String

showList :: [LogicalExpression] -> ShowS

Pretty LogicalExpression

Defined in ATP.Pretty.FOL

Methods

pretty :: LogicalExpression -> Doc

prettyList :: [LogicalExpression] -> Doc

FirstOrder LogicalExpression

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: LogicalExpression -> Set Var

free :: LogicalExpression -> Set Var

bound :: LogicalExpression -> Set Var

occursIn :: Var -> LogicalExpression -> Bool

freeIn :: Var -> LogicalExpression -> Bool

boundIn :: Var -> LogicalExpression -> Bool

ground :: LogicalExpression -> Bool

(~=) :: LogicalExpression -> LogicalExpression -> Bool

(?=) :: LogicalExpression -> LogicalExpression -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => LogicalExpression -> AlphaT m LogicalExpression

Simplify LogicalExpression

Simplify the given formula by replacing each of its constructors with corresponding smart constructors.

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: LogicalExpression -> LogicalExpression

data Theorem

A theorem is zero or more axioms and a conjecture.

Constructors

Theorem

Fields

• axioms :: [Formula]
• conjecture :: Formula

Instances

Eq Theorem

Defined in ATP.FirstOrder.Core

Methods

(==) :: Theorem -> Theorem -> Bool

(/=) :: Theorem -> Theorem -> Bool

Ord Theorem

Defined in ATP.FirstOrder.Core

Methods

compare :: Theorem -> Theorem -> Ordering

(<) :: Theorem -> Theorem -> Bool

(<=) :: Theorem -> Theorem -> Bool

(>) :: Theorem -> Theorem -> Bool

(>=) :: Theorem -> Theorem -> Bool

max :: Theorem -> Theorem -> Theorem

min :: Theorem -> Theorem -> Theorem

Show Theorem

Defined in ATP.FirstOrder.Core

Methods

showsPrec :: Int -> Theorem -> ShowS

show :: Theorem -> String

showList :: [Theorem] -> ShowS

Pretty Theorem

Defined in ATP.Pretty.FOL

Methods

pretty :: Theorem -> Doc

prettyList :: [Theorem] -> Doc

Simplify Theorem

Simplify the given theorem by flattening the conjunction of its premises and its conjecture.

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Theorem -> Theorem

Syntactic sugar

Instances, type synonyms and pattern synonyms for syntactic convenience.

type Function = [Term] -> Term

The type of a function symbol - a mapping from zero or more terms to a term.

type Constant = Term

The type of a constant symbol.

type UnaryFunction = Term -> Term

The type of a function symbol with one argument.

type BinaryFunction = Term -> Term -> Term

The type of a function symbol with two arguments.

type TernaryFunction = Term -> Term -> Term -> Term

The type of a function symbol with three arguments.

pattern Constant :: FunctionSymbol -> Constant

Build a proposition from a predicate symbol.

pattern UnaryFunction :: FunctionSymbol -> UnaryFunction

Build a unary function from a function symbol.

pattern BinaryFunction :: FunctionSymbol -> BinaryFunction

Build a binary function from a function symbol.

pattern TernaryFunction :: FunctionSymbol -> TernaryFunction

Build a ternary function from a function symbol.

type Predicate = [Term] -> Formula

The type of a predicate symbol - a mapping from zero or more terms to a formula.

type Proposition = Formula

The type of a proposition.

type UnaryPredicate = Term -> Formula

The type of a predicate symbol with one argument.

type BinaryPredicate = Term -> Term -> Formula

The type of a predicate symbol with two arguments.

type TernaryPredicate = Term -> Term -> Term -> Formula

The type of a function symbol with three arguments.

pattern Proposition :: PredicateSymbol -> Proposition

Build a proposition from a predicate symbol.

pattern UnaryPredicate :: PredicateSymbol -> UnaryPredicate

Build a unary predicate from a predicate symbol.

pattern BinaryPredicate :: PredicateSymbol -> BinaryPredicate

Build a binary predicate from a predicate symbol.

pattern TernaryPredicate :: PredicateSymbol -> TernaryPredicate

Build a ternary predicate from a predicate symbol.

pattern TautologyLiteral :: Signed Literal

The positive tautology literal.

pattern FalsityLiteral :: Signed Literal

The positive falsity literal.

pattern EmptyClause :: Clause

The empty clause. EmptyClause is semantically (but not syntactically) equivalent to Falsity.

pattern UnitClause :: Signed Literal -> Clause

The unit clause.

pattern TautologyClause :: Clause

A unit clause with a single positive tautology literal. TautologyClause is semantically (but not syntactically) equivalent to Tautology.

pattern NoClauses :: Clauses

The set of clauses with a single clause in it.

pattern SingleClause :: Clause -> Clauses

The set of clauses with a single clause in it.

pattern Tautology :: Formula

The logical tautology.

pattern Falsity :: Formula

The logical false. Falsity is semantically (but not syntactically) equivalent to EmptyClause.

pattern Claim :: Formula -> Theorem

A logical claim is a conjecture entailed by the empty set of axioms.

data AlphaT m a

The monad transformer that adds to the given monad m the ability to track a renaming of free and bound variables in a first-order expression.

Instances

MonadTrans AlphaT

Defined in ATP.FirstOrder.Alpha

Methods

lift :: Monad m => m a -> AlphaT m a

Monad m => Monad (AlphaT m)

Defined in ATP.FirstOrder.Alpha

Methods

(>>=) :: AlphaT m a -> (a -> AlphaT m b) -> AlphaT m b

(>>) :: AlphaT m a -> AlphaT m b -> AlphaT m b

return :: a -> AlphaT m a

Functor m => Functor (AlphaT m)

Defined in ATP.FirstOrder.Alpha

Methods

fmap :: (a -> b) -> AlphaT m a -> AlphaT m b

(<$) :: a -> AlphaT m b -> AlphaT m a

Monad m => Applicative (AlphaT m)

Defined in ATP.FirstOrder.Alpha

Methods

pure :: a -> AlphaT m a

(<*>) :: AlphaT m (a -> b) -> AlphaT m a -> AlphaT m b

liftA2 :: (a -> b -> c) -> AlphaT m a -> AlphaT m b -> AlphaT m c

(*>) :: AlphaT m a -> AlphaT m b -> AlphaT m b

(<*) :: AlphaT m a -> AlphaT m b -> AlphaT m a

evalAlphaT :: Monad m => AlphaT m a -> m a

Evaluate an alpha computation and return the final value, discarding the global scope.

type Alpha a = AlphaT Identity a

The alpha monad parametrized by the type a of the return value.

evalAlpha :: Alpha a -> a

Evaluate an Alpha computation and return the final value, discarding the final variable renaming.

lookup :: Monad m => Var -> AlphaT m (Maybe Var)

Lookup a variable, first in the stack of bound variables, then in the global scope.

scope :: Monad m => AlphaT m [Var]

Read the set of free and bound variables of the given AlphaT computation.

enter :: Monad m => Var -> Var -> AlphaT m a -> AlphaT m a

Run a computation inside AlphaT with the variable renaming.

share :: Monad m => Var -> Var -> AlphaT m ()

Update the global scope with a variable renaming.

class Monad m => MonadAlpha m where

A helper monad for computations on free and bound occurrences of variables.

Methods

binding :: Var -> AlphaT m Var

A monadic action to perform on a variable under a quantifier.

occurrence :: Var -> AlphaT m Var

A monadic action to perform on a variable occurrence.

Smart constructors

signed :: Sign -> Literal -> Signed Literal

A smart constructor for a signed literal.

unitClause :: Signed Literal -> Clause

A smart constructor for a unit clause.

clause :: Foldable f => f (Signed Literal) -> Clause

A smart contructor for a clause. clause eliminates negated boolean constants, falsums and redundant tautologies.

singleClause :: Clause -> Clauses

A smart constructor for a set of clauses with a single clause in it.

clauses :: Foldable f => f Clause -> Clauses

A smart constructor for the set of clauses. clauses eliminates negated boolean constants, falsums and redundant tautologies.

(===) :: Term -> Term -> Formula infix 8

A smart constructor for equality.

(=/=) :: Term -> Term -> Formula infix 8

A smart constructor for inequality.

neg :: Formula -> Formula

A smart constructor for negation.

(\/) :: Formula -> Formula -> Formula infixl 6

A smart constructor for the Or connective. (\/) has the following properties.

Associativity

(f \/ g) \/ h == f \/ (g \/ h)

Left identity

Falsity \/ g == g

Right identity

f \/ Falsity == f

Left zero

Tautology \/ g == Tautology

Right zero

f \/ Tautology == Tautology

(/\) :: Formula -> Formula -> Formula infixl 7

A smart contructor for the And connective. (/\) has the following properties.

Associativity

(f /\ g) /\ h == f /\ (g /\ h)

Left identity

Tautology /\ g == g

Right identity

f /\ Tautology == f

Left zero

Falsity /\ g == Falsity

Right zero

f /\ Falsity == Falsity

(==>) :: Formula -> Formula -> Formula infix 5

A smart constructor for the Implies connective.

(<=>) :: Formula -> Formula -> Formula infixl 5

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

(<~>) :: Formula -> Formula -> Formula infixl 5

A smart constructor for the Xor connective. (<~>) has the following properties.

Associativity

(f <~> g) <~> h == f <~> (g <~> h)

Left identity

Falsity <~> g == g

Right identity

f <~> Falsity == f

class Binder b where

A class of binders for quantified variables.

This class and its instances provides machinery for using polyvariadic functions as higher-order 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]))))

Methods

quantified :: Quantifier -> b -> Formula

A smart constructor for quantified formulas.

Instances

Binder Formula

The degenerate instance - no variable is bound.

Defined in ATP.FirstOrder.Smart

Methods

quantified :: Quantifier -> Formula -> Formula

Binder b => Binder (Term -> b)

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

Methods

quantified :: Quantifier -> (Term -> b) -> Formula

Binder (Var, Formula)

The trivial instance - binder of the varible with the given name.

Defined in ATP.FirstOrder.Smart

Methods

quantified :: Quantifier -> (Var, Formula) -> Formula

forall :: Binder b => b -> Formula

A smart constructor for universally quantified formulas. Provides a polyvariadic higher-order abstract syntax for the bindings of universally quantified variables.

exists :: Binder b => b -> Formula

A smart constructor for existentially quantified formulas. Provides a polyvariadic higher-order abstract syntax for the bindings of existentially quantified variables.

(|-) :: Foldable f => f Formula -> Formula -> Theorem infix 2

A synonym for Theorem.

Monoids

newtype Conjunction

The (Tautology, /\) monoid.

Constructors

Conjunction

Fields

• getConjunction :: Formula

Instances

Eq Conjunction

Defined in ATP.FirstOrder.Smart

Methods

(==) :: Conjunction -> Conjunction -> Bool

(/=) :: Conjunction -> Conjunction -> Bool

Ord Conjunction

Defined in ATP.FirstOrder.Smart

Methods

compare :: Conjunction -> Conjunction -> Ordering

(<) :: Conjunction -> Conjunction -> Bool

(<=) :: Conjunction -> Conjunction -> Bool

(>) :: Conjunction -> Conjunction -> Bool

(>=) :: Conjunction -> Conjunction -> Bool

max :: Conjunction -> Conjunction -> Conjunction

min :: Conjunction -> Conjunction -> Conjunction

Show Conjunction

Defined in ATP.FirstOrder.Smart

Methods

showsPrec :: Int -> Conjunction -> ShowS

show :: Conjunction -> String

showList :: [Conjunction] -> ShowS

Semigroup Conjunction

Defined in ATP.FirstOrder.Smart

Methods

(<>) :: Conjunction -> Conjunction -> Conjunction

sconcat :: NonEmpty Conjunction -> Conjunction

stimes :: Integral b => b -> Conjunction -> Conjunction

Monoid Conjunction

Defined in ATP.FirstOrder.Smart

Methods

mempty :: Conjunction

mappend :: Conjunction -> Conjunction -> Conjunction

mconcat :: [Conjunction] -> Conjunction

conjunction :: Foldable f => f Formula -> Formula

Build the conjunction of formulas in a list.

newtype Disjunction

The (Falsity, \/) monoid.

Constructors

Disjunction

Fields

• getDisjunction :: Formula

Instances

Eq Disjunction

Defined in ATP.FirstOrder.Smart

Methods

(==) :: Disjunction -> Disjunction -> Bool

(/=) :: Disjunction -> Disjunction -> Bool

Ord Disjunction

Defined in ATP.FirstOrder.Smart

Methods

compare :: Disjunction -> Disjunction -> Ordering

(<) :: Disjunction -> Disjunction -> Bool

(<=) :: Disjunction -> Disjunction -> Bool

(>) :: Disjunction -> Disjunction -> Bool

(>=) :: Disjunction -> Disjunction -> Bool

max :: Disjunction -> Disjunction -> Disjunction

min :: Disjunction -> Disjunction -> Disjunction

Show Disjunction

Defined in ATP.FirstOrder.Smart

Methods

showsPrec :: Int -> Disjunction -> ShowS

show :: Disjunction -> String

showList :: [Disjunction] -> ShowS

Semigroup Disjunction

Defined in ATP.FirstOrder.Smart

Methods

(<>) :: Disjunction -> Disjunction -> Disjunction

sconcat :: NonEmpty Disjunction -> Disjunction

stimes :: Integral b => b -> Disjunction -> Disjunction

Monoid Disjunction

Defined in ATP.FirstOrder.Smart

Methods

mempty :: Disjunction

mappend :: Disjunction -> Disjunction -> Disjunction

mconcat :: [Disjunction] -> Disjunction

disjunction :: Foldable f => f Formula -> Formula

Build the disjunction of formulas in a list.

newtype Equivalence

The (Tautology, <=>) monoid.

Constructors

Equivalence

Fields

• getEquivalence :: Formula

Instances

Eq Equivalence

Defined in ATP.FirstOrder.Smart

Methods

(==) :: Equivalence -> Equivalence -> Bool

(/=) :: Equivalence -> Equivalence -> Bool

Ord Equivalence

Defined in ATP.FirstOrder.Smart

Methods

compare :: Equivalence -> Equivalence -> Ordering

(<) :: Equivalence -> Equivalence -> Bool

(<=) :: Equivalence -> Equivalence -> Bool

(>) :: Equivalence -> Equivalence -> Bool

(>=) :: Equivalence -> Equivalence -> Bool

max :: Equivalence -> Equivalence -> Equivalence

min :: Equivalence -> Equivalence -> Equivalence

Show Equivalence

Defined in ATP.FirstOrder.Smart

Methods

showsPrec :: Int -> Equivalence -> ShowS

show :: Equivalence -> String

showList :: [Equivalence] -> ShowS

Semigroup Equivalence

Defined in ATP.FirstOrder.Smart

Methods

(<>) :: Equivalence -> Equivalence -> Equivalence

sconcat :: NonEmpty Equivalence -> Equivalence

stimes :: Integral b => b -> Equivalence -> Equivalence

Monoid Equivalence

Defined in ATP.FirstOrder.Smart

Methods

mempty :: Equivalence

mappend :: Equivalence -> Equivalence -> Equivalence

mconcat :: [Equivalence] -> Equivalence

equivalence :: Foldable f => f Formula -> Formula

Build the equivalence of formulas in a list.

newtype Inequivalence

The (Falsity, <~>) monoid.

Constructors

Inequivalence

Fields

• getInequivalence :: Formula

Instances

Eq Inequivalence

Defined in ATP.FirstOrder.Smart

Methods

(==) :: Inequivalence -> Inequivalence -> Bool

(/=) :: Inequivalence -> Inequivalence -> Bool

Ord Inequivalence

Defined in ATP.FirstOrder.Smart

Methods

compare :: Inequivalence -> Inequivalence -> Ordering

(<) :: Inequivalence -> Inequivalence -> Bool

(<=) :: Inequivalence -> Inequivalence -> Bool

(>) :: Inequivalence -> Inequivalence -> Bool

(>=) :: Inequivalence -> Inequivalence -> Bool

max :: Inequivalence -> Inequivalence -> Inequivalence

min :: Inequivalence -> Inequivalence -> Inequivalence

Show Inequivalence

Defined in ATP.FirstOrder.Smart

Methods

showsPrec :: Int -> Inequivalence -> ShowS

show :: Inequivalence -> String

showList :: [Inequivalence] -> ShowS

Semigroup Inequivalence

Defined in ATP.FirstOrder.Smart

Methods

(<>) :: Inequivalence -> Inequivalence -> Inequivalence

sconcat :: NonEmpty Inequivalence -> Inequivalence

stimes :: Integral b => b -> Inequivalence -> Inequivalence

Monoid Inequivalence

Defined in ATP.FirstOrder.Smart

Methods

mempty :: Inequivalence

mappend :: Inequivalence -> Inequivalence -> Inequivalence

mconcat :: [Inequivalence] -> Inequivalence

inequivalence :: Foldable f => f Formula -> Formula

Build the inequivalence of formulas in a list.

Miscellaneous

flattenConjunction :: Foldable f => f Formula -> [Formula]

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]

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

A class of first-order expressions that simplify syntactically shrinks while preserving their evaluation.

Methods

simplify :: a -> a

Instances

Simplify Theorem

Simplify the given theorem by flattening the conjunction of its premises and its conjecture.

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Theorem -> Theorem

Simplify LogicalExpression

Simplify the given formula by replacing each of its constructors with corresponding smart constructors.

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: LogicalExpression -> LogicalExpression

Simplify Formula

Simplify the given formula by replacing each of its constructors with corresponding smart constructors. The effects of simplification are the following.

• simplify f does not contain nested negations.
• simplify f does not contain some of the constant atomic formulas from f.
• All chained applications of any binary connective inside simplify f are right-associative.

Any formula built only using smart constructors is simplified by construction.

>>> simplify (Connected Or tautology (Atomic (Predicate "p" [])))
Atomic (Propositional True)

>>> simplify (Negate (Negate (Atomic (Predicate "p" []))))
Atomic (Predicate "p" [])

>>> simplify (Connected And (Connected And (Atomic (Predicate "p" [])) (Atomic (Predicate "q" []))) (Atomic (Predicate "r" [])))
Connected And (Atomic (Predicate "p" [])) (Connected And (Atomic (Predicate "q" [])) (Atomic (Predicate "r" [])))

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Formula -> Formula

Simplify Clauses

Simplify the given clause set by replacing the Clauses constructor with the smart constructor clauses. The effects of simplification are the following.

• simplify c does not contain negative constant literals.
• simplify c does not contain falsum literals.
• simplify c does not contain tautology literals.
• simplify c does not contain redundant falsum literals.

>>> simplify (SingleClause (UnitClause (Signed Negative (Propositional True))))
Clauses {getClauses = [Literals {getLiterals = []}]}

>>> simplify (SingleClause (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])]))
Clauses {getClauses = [Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}]}

>>> simplify (SingleClause (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])]))
Clauses {getClauses = []}

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Clauses -> Clauses

Simplify Clause

Simplify the given clause by replacing the Literals constructor with the smart constructor clause. The effects of simplification are the following.

• simplify c does not contain negative constant literals.
• simplify c does not contain falsum literals.
• simplify c does not contain redundant tautology literals.

>>> simplify (UnitClause (Signed Negative (Propositional True)))
Literals {getLiterals = []}

>>> simplify (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])])
Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}

>>> simplify (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])])
Literals {getLiterals = [Signed {signof = Positive, unsign = Propositional True}]}

Defined in ATP.FirstOrder.Simplification

Methods

simplify :: Clause -> Clause

Occurrence

class FirstOrder e where

A class of first-order expressions, i.e. expressions that might contain variables. Formulas, Literals and Terms are first-order expressions.

A variable can occur both as free and bound, therefore free e and bound e are not necessarily disjoint and v freeIn e and v boundIn e are not necessarily musually exclusive.

vars, free and bound are connected by the following property.

free e <> bound e == vars e

occursIn, freeIn and boundIn are connected by the following property.

v `freeIn` e || v `boundIn` e == v `occursIn` e

Minimal complete definition

vars, free, bound, (?=), alpha

Methods

vars :: e -> Set Var

The set of all variables that occur anywhere in the given expression.

free :: e -> Set Var

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

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

Check whether the given variable occurs anywhere in the given expression.

freeIn :: Var -> e -> Bool

Check whether the given variable occurs freely anywhere in the given expression.

boundIn :: Var -> e -> Bool

Check whether the given variable occurs bound anywhere in the given expression.

ground :: e -> Bool

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

Check whether two given expressions are alpha-equivalent, 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

A helper function calculating alpha-equivalence using the Alpha monad stack.

alpha :: MonadAlpha m => e -> AlphaT m e

Instances

FirstOrder LogicalExpression

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: LogicalExpression -> Set Var

free :: LogicalExpression -> Set Var

bound :: LogicalExpression -> Set Var

occursIn :: Var -> LogicalExpression -> Bool

freeIn :: Var -> LogicalExpression -> Bool

boundIn :: Var -> LogicalExpression -> Bool

ground :: LogicalExpression -> Bool

(~=) :: LogicalExpression -> LogicalExpression -> Bool

(?=) :: LogicalExpression -> LogicalExpression -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => LogicalExpression -> AlphaT m LogicalExpression

FirstOrder Formula

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Formula -> Set Var

free :: Formula -> Set Var

bound :: Formula -> Set Var

occursIn :: Var -> Formula -> Bool

freeIn :: Var -> Formula -> Bool

boundIn :: Var -> Formula -> Bool

ground :: Formula -> Bool

(~=) :: Formula -> Formula -> Bool

(?=) :: Formula -> Formula -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Formula -> AlphaT m Formula

FirstOrder Clause

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Clause -> Set Var

free :: Clause -> Set Var

bound :: Clause -> Set Var

occursIn :: Var -> Clause -> Bool

freeIn :: Var -> Clause -> Bool

boundIn :: Var -> Clause -> Bool

ground :: Clause -> Bool

(~=) :: Clause -> Clause -> Bool

(?=) :: Clause -> Clause -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Clause -> AlphaT m Clause

FirstOrder Literal

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Literal -> Set Var

free :: Literal -> Set Var

bound :: Literal -> Set Var

occursIn :: Var -> Literal -> Bool

freeIn :: Var -> Literal -> Bool

boundIn :: Var -> Literal -> Bool

ground :: Literal -> Bool

(~=) :: Literal -> Literal -> Bool

(?=) :: Literal -> Literal -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Literal -> AlphaT m Literal

FirstOrder Term

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Term -> Set Var

free :: Term -> Set Var

bound :: Term -> Set Var

occursIn :: Var -> Term -> Bool

freeIn :: Var -> Term -> Bool

boundIn :: Var -> Term -> Bool

ground :: Term -> Bool

(~=) :: Term -> Term -> Bool

(?=) :: Term -> Term -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Term -> AlphaT m Term

FirstOrder Var

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Var -> Set Var

free :: Var -> Set Var

bound :: Var -> Set Var

occursIn :: Var -> Var -> Bool

freeIn :: Var -> Var -> Bool

boundIn :: Var -> Var -> Bool

ground :: Var -> Bool

(~=) :: Var -> Var -> Bool

(?=) :: Var -> Var -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Var -> AlphaT m Var

FirstOrder e => FirstOrder [e]

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: [e] -> Set Var

free :: [e] -> Set Var

bound :: [e] -> Set Var

occursIn :: Var -> [e] -> Bool

freeIn :: Var -> [e] -> Bool

boundIn :: Var -> [e] -> Bool

ground :: [e] -> Bool

(~=) :: [e] -> [e] -> Bool

(?=) :: [e] -> [e] -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => [e] -> AlphaT m [e]

FirstOrder e => FirstOrder (Signed e)

Defined in ATP.FirstOrder.Occurrence

Methods

vars :: Signed e -> Set Var

free :: Signed e -> Set Var

bound :: Signed e -> Set Var

occursIn :: Var -> Signed e -> Bool

freeIn :: Var -> Signed e -> Bool

boundIn :: Var -> Signed e -> Bool

ground :: Signed e -> Bool

(~=) :: Signed e -> Signed e -> Bool

(?=) :: Signed e -> Signed e -> Alpha Bool

alpha :: forall (m :: Type -> Type). MonadAlpha m => Signed e -> AlphaT m (Signed e)

closed :: Formula -> Bool

Check whether the given formula is closed, i.e. does not contain any free variables.

close :: Formula -> Formula

Make any given formula closed by adding a top-level universal quantifier for each of its free variables.

close and unprefix are connected by the following property.

unprefix (close f) === f

unprefix :: Formula -> Formula

Remove the top-level 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

Convert a signed literal to a (negated) atomic formula.

unliftSignedLiteral :: Formula -> Maybe (Signed Literal)

Try to convert a first-order formula f to a signed literal. This function succeeds if f is a (negated) atomic formula.

liftClause :: Clause -> Formula

Convert a clause to a full first-order formula.

unliftClause :: Formula -> Maybe Clause

Try to convert a first-order 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

Convert a contradiction to an inference.

unliftContradiction :: Inference f -> Maybe (Contradiction f)

Try to convert an inference to a contradiction.

liftRefutation :: Ord f => f -> Refutation f -> Derivation f

Convert a refutation to a derivation.

unliftRefutation :: Derivation f -> Maybe (Refutation f)

Try to convert a derivation to a refutation. This function succeds if the derivation has exactly one inference resulting in contradiction.

Proofs

data Rule f

The inference rule.

Constructors

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

Defined in ATP.FirstOrder.Derivation

Methods

fmap :: (a -> b) -> Rule a -> Rule b

(<$) :: a -> Rule b -> Rule a

Foldable Rule

Defined in ATP.FirstOrder.Derivation

Methods

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

toList :: Rule a -> [a]

null :: Rule a -> Bool

length :: Rule a -> Int

elem :: Eq a => a -> Rule a -> Bool

maximum :: Ord a => Rule a -> a

minimum :: Ord a => Rule a -> a

sum :: Num a => Rule a -> a

product :: Num a => Rule a -> a

Traversable Rule

Defined in ATP.FirstOrder.Derivation

Methods

traverse :: Applicative f => (a -> f b) -> Rule a -> f (Rule b)

sequenceA :: Applicative f => Rule (f a) -> f (Rule a)

mapM :: Monad m => (a -> m b) -> Rule a -> m (Rule b)

sequence :: Monad m => Rule (m a) -> m (Rule a)

Eq f => Eq (Rule f)

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: Rule f -> Rule f -> Bool

(/=) :: Rule f -> Rule f -> Bool

Ord f => Ord (Rule f)

Defined in ATP.FirstOrder.Derivation

Methods

compare :: Rule f -> Rule f -> Ordering

(<) :: Rule f -> Rule f -> Bool

(<=) :: Rule f -> Rule f -> Bool

(>) :: Rule f -> Rule f -> Bool

(>=) :: Rule f -> Rule f -> Bool

max :: Rule f -> Rule f -> Rule f

min :: Rule f -> Rule f -> Rule f

Show f => Show (Rule f)

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> Rule f -> ShowS

show :: Rule f -> String

showList :: [Rule f] -> ShowS

Pretty l => Pretty (Rule l)

Defined in ATP.Pretty.FOL

Methods

pretty :: Rule l -> Doc

prettyList :: [Rule l] -> Doc

newtype RuleName

The name of an inference rule.

Constructors

RuleName

Fields

• unRuleName :: Text

Instances

Eq RuleName

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: RuleName -> RuleName -> Bool

(/=) :: RuleName -> RuleName -> Bool

Ord RuleName

Defined in ATP.FirstOrder.Derivation

Methods

compare :: RuleName -> RuleName -> Ordering

(<) :: RuleName -> RuleName -> Bool

(<=) :: RuleName -> RuleName -> Bool

(>) :: RuleName -> RuleName -> Bool

(>=) :: RuleName -> RuleName -> Bool

max :: RuleName -> RuleName -> RuleName

min :: RuleName -> RuleName -> RuleName

Show RuleName

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> RuleName -> ShowS

show :: RuleName -> String

showList :: [RuleName] -> ShowS

IsString RuleName

Defined in ATP.FirstOrder.Derivation

Methods

fromString :: String -> RuleName

Pretty RuleName

Defined in ATP.Pretty.FOL

Methods

pretty :: RuleName -> Doc

prettyList :: [RuleName] -> Doc

ruleName :: Rule f -> RuleName

The name of the given inference rule.

>>> unRuleName (ruleName AxiomOfChoice)
"axiom of choice"

data Inference f

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.

Constructors

Inference

Fields

• inferenceRule :: Rule f
• consequent :: LogicalExpression

Instances

Functor Inference

Defined in ATP.FirstOrder.Derivation

Methods

fmap :: (a -> b) -> Inference a -> Inference b

(<$) :: a -> Inference b -> Inference a

Foldable Inference

Defined in ATP.FirstOrder.Derivation

Methods

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]

null :: Inference a -> Bool

length :: Inference a -> Int

elem :: Eq a => a -> Inference a -> Bool

maximum :: Ord a => Inference a -> a

minimum :: Ord a => Inference a -> a

sum :: Num a => Inference a -> a

product :: Num a => Inference a -> a

Traversable Inference

Defined in ATP.FirstOrder.Derivation

Methods

traverse :: Applicative f => (a -> f b) -> Inference a -> f (Inference b)

sequenceA :: Applicative f => Inference (f a) -> f (Inference a)

mapM :: Monad m => (a -> m b) -> Inference a -> m (Inference b)

sequence :: Monad m => Inference (m a) -> m (Inference a)

Eq f => Eq (Inference f)

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: Inference f -> Inference f -> Bool

(/=) :: Inference f -> Inference f -> Bool

Ord f => Ord (Inference f)

Defined in ATP.FirstOrder.Derivation

Methods

compare :: Inference f -> Inference f -> Ordering

(<) :: Inference f -> Inference f -> Bool

(<=) :: Inference f -> Inference f -> Bool

(>) :: Inference f -> Inference f -> Bool

(>=) :: Inference f -> Inference f -> Bool

max :: Inference f -> Inference f -> Inference f

min :: Inference f -> Inference f -> Inference f

Show f => Show (Inference f)

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> Inference f -> ShowS

show :: Inference f -> String

showList :: [Inference f] -> ShowS

Pretty l => Pretty (Inference l)

Defined in ATP.Pretty.FOL

Methods

pretty :: Inference l -> Doc

prettyList :: [Inference l] -> Doc

antecedents :: Inference f -> [f]

The antecedents of an inference.

newtype Contradiction f

Contradiction is a special case of an inference that has the logical falsum as the consequent.

Constructors

Contradiction (Rule f)

Instances

Functor Contradiction

Defined in ATP.FirstOrder.Derivation

Methods

fmap :: (a -> b) -> Contradiction a -> Contradiction b

(<$) :: a -> Contradiction b -> Contradiction a

Foldable Contradiction

Defined in ATP.FirstOrder.Derivation

Methods

fold :: Monoid m => Contradiction m -> m

foldMap :: Monoid m => (a -> m) -> Contradiction a -> m

foldMap' :: Monoid m => (a -> m) -> Contradiction a -> m

foldr :: (a -> b -> b) -> b -> Contradiction a -> b

foldr' :: (a -> b -> b) -> b -> Contradiction a -> b

foldl :: (b -> a -> b) -> b -> Contradiction a -> b

foldl' :: (b -> a -> b) -> b -> Contradiction a -> b

foldr1 :: (a -> a -> a) -> Contradiction a -> a

foldl1 :: (a -> a -> a) -> Contradiction a -> a

toList :: Contradiction a -> [a]

null :: Contradiction a -> Bool

length :: Contradiction a -> Int

elem :: Eq a => a -> Contradiction a -> Bool

maximum :: Ord a => Contradiction a -> a

minimum :: Ord a => Contradiction a -> a

sum :: Num a => Contradiction a -> a

product :: Num a => Contradiction a -> a

Traversable Contradiction

Defined in ATP.FirstOrder.Derivation

Methods

traverse :: Applicative f => (a -> f b) -> Contradiction a -> f (Contradiction b)

sequenceA :: Applicative f => Contradiction (f a) -> f (Contradiction a)

mapM :: Monad m => (a -> m b) -> Contradiction a -> m (Contradiction b)

sequence :: Monad m => Contradiction (m a) -> m (Contradiction a)

Eq f => Eq (Contradiction f)

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: Contradiction f -> Contradiction f -> Bool

(/=) :: Contradiction f -> Contradiction f -> Bool

Ord f => Ord (Contradiction f)

Defined in ATP.FirstOrder.Derivation

Methods

compare :: Contradiction f -> Contradiction f -> Ordering

(<) :: Contradiction f -> Contradiction f -> Bool

(<=) :: Contradiction f -> Contradiction f -> Bool

(>) :: Contradiction f -> Contradiction f -> Bool

(>=) :: Contradiction f -> Contradiction f -> Bool

max :: Contradiction f -> Contradiction f -> Contradiction f

min :: Contradiction f -> Contradiction f -> Contradiction f

Show f => Show (Contradiction f)

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> Contradiction f -> ShowS

show :: Contradiction f -> String

showList :: [Contradiction f] -> ShowS

data Sequent f

A sequent is a logical inference, annotated with a label. Linked sequents form derivations.

Constructors

Sequent f (Inference f)

Instances

Functor Sequent

Defined in ATP.FirstOrder.Derivation

Methods

fmap :: (a -> b) -> Sequent a -> Sequent b

(<$) :: a -> Sequent b -> Sequent a

Foldable Sequent

Defined in ATP.FirstOrder.Derivation

Methods

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

toList :: Sequent a -> [a]

null :: Sequent a -> Bool

length :: Sequent a -> Int

elem :: Eq a => a -> Sequent a -> Bool

maximum :: Ord a => Sequent a -> a

minimum :: Ord a => Sequent a -> a

sum :: Num a => Sequent a -> a

product :: Num a => Sequent a -> a

Traversable Sequent

Defined in ATP.FirstOrder.Derivation

Methods

traverse :: Applicative f => (a -> f b) -> Sequent a -> f (Sequent b)

sequenceA :: Applicative f => Sequent (f a) -> f (Sequent a)

mapM :: Monad m => (a -> m b) -> Sequent a -> m (Sequent b)

sequence :: Monad m => Sequent (m a) -> m (Sequent a)

Eq f => Eq (Sequent f)

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: Sequent f -> Sequent f -> Bool

(/=) :: Sequent f -> Sequent f -> Bool

Ord f => Ord (Sequent f)

Defined in ATP.FirstOrder.Derivation

Methods

compare :: Sequent f -> Sequent f -> Ordering

(<) :: Sequent f -> Sequent f -> Bool

(<=) :: Sequent f -> Sequent f -> Bool

(>) :: Sequent f -> Sequent f -> Bool

(>=) :: Sequent f -> Sequent f -> Bool

max :: Sequent f -> Sequent f -> Sequent f

min :: Sequent f -> Sequent f -> Sequent f

Show f => Show (Sequent f)

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> Sequent f -> ShowS

show :: Sequent f -> String

showList :: [Sequent f] -> ShowS

Pretty l => Pretty (Sequent l)

Defined in ATP.Pretty.FOL

Methods

pretty :: Sequent l -> Doc

prettyList :: [Sequent l] -> Doc

newtype Derivation f

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.

Constructors

Derivation (Map f (Inference f))

Instances

Eq f => Eq (Derivation f)

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: Derivation f -> Derivation f -> Bool

(/=) :: Derivation f -> Derivation f -> Bool

Ord f => Ord (Derivation f)

Defined in ATP.FirstOrder.Derivation

Methods

compare :: Derivation f -> Derivation f -> Ordering

(<) :: Derivation f -> Derivation f -> Bool

(<=) :: Derivation f -> Derivation f -> Bool

(>) :: Derivation f -> Derivation f -> Bool

(>=) :: Derivation f -> Derivation f -> Bool

max :: Derivation f -> Derivation f -> Derivation f

min :: Derivation f -> Derivation f -> Derivation f

Show f => Show (Derivation f)

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> Derivation f -> ShowS

show :: Derivation f -> String

showList :: [Derivation f] -> ShowS

Ord f => Semigroup (Derivation f)

Defined in ATP.FirstOrder.Derivation

Methods

(<>) :: Derivation f -> Derivation f -> Derivation f

sconcat :: NonEmpty (Derivation f) -> Derivation f

stimes :: Integral b => b -> Derivation f -> Derivation f

Ord f => Monoid (Derivation f)

Defined in ATP.FirstOrder.Derivation

Methods

mempty :: Derivation f

mappend :: Derivation f -> Derivation f -> Derivation f

mconcat :: [Derivation f] -> Derivation f

(Ord l, Pretty l) => Pretty (Derivation l)

Defined in ATP.Pretty.FOL

Methods

pretty :: Derivation l -> Doc

prettyList :: [Derivation l] -> Doc

addSequent :: Ord f => Derivation f -> Sequent f -> Derivation f

Attach a sequent to a derivation.

breadthFirst :: Ord f => Derivation f -> [Sequent f]

Traverse the given derivation breadth-first and produce a list of sequents.

labeling :: Ord f => [Sequent f] -> Map f LogicalExpression

Construct a mapping between inference labels and their correspondent formulas.

data Refutation f

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.

Constructors

Refutation (Derivation f) (Contradiction f)

Instances

Eq f => Eq (Refutation f)

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: Refutation f -> Refutation f -> Bool

(/=) :: Refutation f -> Refutation f -> Bool

Ord f => Ord (Refutation f)

Defined in ATP.FirstOrder.Derivation

Methods

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)

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> Refutation f -> ShowS

show :: Refutation f -> String

showList :: [Refutation f] -> ShowS

(Ord l, Pretty l) => Pretty (Refutation l)

Defined in ATP.Pretty.FOL

Methods

pretty :: Refutation l -> Doc

prettyList :: [Refutation l] -> Doc

data Solution

The solution produced by an automated first-order theorem prover.

Constructors

Saturation (Derivation Integer)

A theorem can be disproven if the prover constructs a saturated set of first-order 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.

Instances

Eq Solution

Defined in ATP.FirstOrder.Derivation

Methods

(==) :: Solution -> Solution -> Bool

(/=) :: Solution -> Solution -> Bool

Ord Solution

Defined in ATP.FirstOrder.Derivation

Methods

compare :: Solution -> Solution -> Ordering

(<) :: Solution -> Solution -> Bool

(<=) :: Solution -> Solution -> Bool

(>) :: Solution -> Solution -> Bool

(>=) :: Solution -> Solution -> Bool

max :: Solution -> Solution -> Solution

min :: Solution -> Solution -> Solution

Show Solution

Defined in ATP.FirstOrder.Derivation

Methods

showsPrec :: Int -> Solution -> ShowS

show :: Solution -> String

showList :: [Solution] -> ShowS

Pretty Solution

Defined in ATP.Pretty.FOL

Methods

pretty :: Solution -> Doc

prettyList :: [Solution] -> Doc