Copyright	(c) Artem Mavrin 2021
License	BSD3
Maintainer	artemvmavrin@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

AutoProof.Classical

Contents

Formulas
- Operations on formulas
Judgements
- Judgement constructor
- Operations on judgements
Proofs
- Provability checking
Satisfiability
Abstract syntax trees
Parsing
Pretty-printing

Description

Classical propositional logic library.

Synopsis

data Formula a where
- pattern Lit :: Bool -> Formula a
- pattern Var :: a -> Formula a
- pattern Not :: Formula a -> Formula a
- pattern Imp :: Formula a -> Formula a -> Formula a
- pattern Or :: Formula a -> Formula a -> Formula a
- pattern And :: Formula a -> Formula a -> Formula a
- pattern Iff :: Formula a -> Formula a -> Formula a
subformulas :: Ord a => Formula a -> Set (Formula a)
substitute :: Eq a => Formula a -> a -> Formula a -> Formula a
canonicalCNF :: Ord a => Formula a -> Formula a
getAnyVariable :: Formula a -> Maybe a
type Context a = Set (Formula a)
data Judgement a = Judgement {
- antecedents :: Context a
- succedent :: Formula a
}
(|-) :: (Ord a, Foldable f) => f (Formula a) -> Formula a -> Judgement a
weakenJudgement :: Ord a => Judgement a -> Formula a -> Judgement a
data Proof a where
- pattern Axiom :: Judgement a -> Proof a
- pattern FalseElim :: Judgement a -> Proof a -> Proof a
- pattern TrueIntr :: Judgement a -> Proof a
- pattern NotElim :: Judgement a -> Proof a -> Proof a -> Proof a
- pattern NotIntr :: Judgement a -> Proof a -> Proof a
- pattern ImpElim :: Judgement a -> Proof a -> Proof a -> Proof a
- pattern ImpIntr :: Judgement a -> Proof a -> Proof a
- pattern OrElim :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a
- pattern OrIntrL :: Judgement a -> Proof a -> Proof a
- pattern OrIntrR :: Judgement a -> Proof a -> Proof a
- pattern AndElimL :: Judgement a -> Proof a -> Proof a
- pattern AndElimR :: Judgement a -> Proof a -> Proof a
- pattern AndIntr :: Judgement a -> Proof a -> Proof a -> Proof a
- pattern IffElimL :: Judgement a -> Proof a -> Proof a
- pattern IffElimR :: Judgement a -> Proof a -> Proof a
- pattern IffIntr :: Judgement a -> Proof a -> Proof a -> Proof a
isProvable :: Ord a => Judgement a -> Bool
isTautology :: Ord a => Formula a -> Bool
class TruthAssignment t a where
- evalVar :: t -> a -> Bool
- evalFormula :: t -> Formula a -> Bool
(|=) :: TruthAssignment t a => t -> Formula a -> Bool
satSimple :: Eq a => Formula a -> Bool
satDPLL :: Ord a => Formula a -> Bool
satAssignmentSimple :: Ord a => Formula a -> Maybe (Map a Bool)
satAssignmentDPLL :: Ord a => Formula a -> Maybe (Map a Bool)
class AST t where
- type Root t
- root :: t -> Root t
- children :: t -> [t]
- height :: t -> Int
- size :: t -> Int
subtrees :: (AST t, Ord t) => t -> Set t
properSubtrees :: (AST t, Ord t) => t -> Set t
parseFormula :: String -> Maybe (Formula String)
parseJudgement :: String -> Maybe (Judgement String)
pretty :: PrettyPrintable a => a -> String
prettyFormula :: PrettyPrintable a => Formula a -> String
prettyJudgement :: PrettyPrintable a => Judgement a -> String
prettyProof :: PrettyPrintable a => Proof a -> String

Formulas

data Formula a where Source #

Formulas of propositional logic are built inductively from atomic propositions

truth $\top$,
falsity $\bot$, and
propositional variables $a, b, c, \ldots$

using the unary connective

negation $\lnot$

and the binary connectives

implication $\rightarrow$,
disjunction $\lor$,
conjunction $\land$, and
equivalence $\leftrightarrow$.

Bundled Patterns

pattern Lit :: Bool -> Formula a	Propositional literal/constant. `(Lit True)` is $\top$ (i.e., truth, tautology, or top), and `(Lit False)` is $\bot$ (i.e., falsity, contradiction, or bottom).
pattern Var :: a -> Formula a	Propositional variable. `(Var x)` represents a propositional variable $x$.
pattern Not :: Formula a -> Formula a	Negation. `(Not p)` represents the formula $\lnot p$.
pattern Imp :: Formula a -> Formula a -> Formula a	Implication. `(Imp p q)` represents the formula $p \rightarrow q$.
pattern Or :: Formula a -> Formula a -> Formula a	Disjunction. `(Or p q)` represents the formula $p \lor q$.
pattern And :: Formula a -> Formula a -> Formula a	Conjunction. `(And p q)` represents the formula $p \land q$.
pattern Iff :: Formula a -> Formula a -> Formula a	Equivalence. `(Iff p q)` represents the formula $p \leftrightarrow q$.

Instances

Instances details

Eq a => Eq (Formula a) Source #	Syntactic equality.
Instance details Defined in AutoProof.Internal.Formula.Types Methods (==) :: Formula a -> Formula a -> Bool # (/=) :: Formula a -> Formula a -> Bool #
Ord a => Ord (Formula a) Source #	First compare heights, then compare sizes, then resolve using the convention `Lit < Var < Not < Imp < Or < And < Iff` (on equality, compare children from left to right).
Instance details Defined in AutoProof.Internal.Formula.Types Methods compare :: Formula a -> Formula a -> Ordering # (<) :: Formula a -> Formula a -> Bool # (<=) :: Formula a -> Formula a -> Bool # (>) :: Formula a -> Formula a -> Bool # (>=) :: Formula a -> Formula a -> Bool # max :: Formula a -> Formula a -> Formula a # min :: Formula a -> Formula a -> Formula a #
Read a => Read (Formula a) Source #
Instance details Defined in AutoProof.Internal.Formula.Types Methods readsPrec :: Int -> ReadS (Formula a) # readList :: ReadS [Formula a] # readPrec :: ReadPrec (Formula a) # readListPrec :: ReadPrec [Formula a] #
Show a => Show (Formula a) Source #
Instance details Defined in AutoProof.Internal.Formula.Types Methods showsPrec :: Int -> Formula a -> ShowS # show :: Formula a -> String # showList :: [Formula a] -> ShowS #
AST (Formula a) Source #
Instance details Defined in AutoProof.Internal.Formula.Types Associated Types type Root (Formula a) Source # Methods root :: Formula a -> Root (Formula a) Source # children :: Formula a -> [Formula a] Source # metadata :: Formula a -> ASTMetadata Source # height :: Formula a -> Int Source # size :: Formula a -> Int Source #
PrettyPrintable a => PrettyPrintable (Formula a) Source #
Instance details Defined in AutoProof.Internal.Formula.Types Methods pretty :: Formula a -> String Source # prettys :: Formula a -> ShowS Source #
type Root (Formula a) Source #
Instance details Defined in AutoProof.Internal.Formula.Types type Root (Formula a) = Maybe a

Operations on formulas

subformulas :: Ord a => Formula a -> Set (Formula a) Source #

Get the set of subformulas of a propositional formula.

Examples

Expand

>>> subformulas $ Or (Var 'x') (And (Var 'y') (Var 'z'))
fromList [Var 'x',Var 'y',Var 'z',And (Var 'y') (Var 'z'),Or (Var 'x') (And (Var 'y') (Var 'z'))]

substitute :: Eq a => Formula a -> a -> Formula a -> Formula a Source #

(substitute a x p) represents $a[p/x]$, the substitution of each occurence of the variable $x$ in the formula $a$ by the formula $p$.

Examples

Expand

>>> substitute (Imp (Var 'e') (Var 'e')) 'e' (And (Var 'a') (Var 'a'))
Imp (And (Var 'a') (Var 'a')) (And (Var 'a') (Var 'a'))

canonicalCNF :: Ord a => Formula a -> Formula a Source #

Convert a formula into a canonical conjunctive normal form.

Examples

Expand

>>> import AutoProof.Internal.Formula
>>> canonicalCNF $ Or (Not (Imp (Var "a") (Var "b"))) (Var "c")
And (Or (Var "c") (Not (Var "b"))) (Or (Var "c") (Var "a"))

getAnyVariable :: Formula a -> Maybe a Source #

Obtain a propositional variable from a formula, if there is one.

Examples

Expand

>>> getAnyVariable (Or (Var "a") (Var "b"))
Just "a"

>>> getAnyVariable (Lit False :: Formula String)
Nothing

Judgements

type Context a = Set (Formula a) Source #

A set of propositional formulas, used as antecedents of a judgement.

data Judgement a Source #

(Judgement c a) represents the judgement or sequent $c \vdash a$.

>>> Judgement Set.empty (Imp (And (Var 'a') (Var 'b')) (Var 'a'))
[] |- Imp (And (Var 'a') (Var 'b')) (Var 'a')

Constructors

Judgement
Fields antecedents :: Context a The antecedents (or hypotheses). succedent :: Formula a The succedent (or consequent, or conclusion).

Instances

Instances details

Eq a => Eq (Judgement a) Source #
Instance details Defined in AutoProof.Internal.Judgement Methods (==) :: Judgement a -> Judgement a -> Bool # (/=) :: Judgement a -> Judgement a -> Bool #
Ord a => Ord (Judgement a) Source #
Instance details Defined in AutoProof.Internal.Judgement Methods compare :: Judgement a -> Judgement a -> Ordering # (<) :: Judgement a -> Judgement a -> Bool # (<=) :: Judgement a -> Judgement a -> Bool # (>) :: Judgement a -> Judgement a -> Bool # (>=) :: Judgement a -> Judgement a -> Bool # max :: Judgement a -> Judgement a -> Judgement a # min :: Judgement a -> Judgement a -> Judgement a #
(Ord a, Read a) => Read (Judgement a) Source #
Instance details Defined in AutoProof.Internal.Judgement Methods readsPrec :: Int -> ReadS (Judgement a) # readList :: ReadS [Judgement a] # readPrec :: ReadPrec (Judgement a) # readListPrec :: ReadPrec [Judgement a] #
Show a => Show (Judgement a) Source #
Instance details Defined in AutoProof.Internal.Judgement Methods showsPrec :: Int -> Judgement a -> ShowS # show :: Judgement a -> String # showList :: [Judgement a] -> ShowS #
PrettyPrintable a => PrettyPrintable (Judgement a) Source #
Instance details Defined in AutoProof.Internal.Judgement Methods pretty :: Judgement a -> String Source # prettys :: Judgement a -> ShowS Source #

Judgement constructor

(|-) :: (Ord a, Foldable f) => f (Formula a) -> Formula a -> Judgement a infix 5 Source #

Infix judgement constructor. (c |- a) represents the judgement $c \vdash a$.

>>> [Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b'
[Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'b'

Note: If c is already a Set, then it is recommended to use (Judgement c a) in favor of (c |- a), since the latter will create a new set and fill it with the values in c.

Operations on judgements

weakenJudgement :: Ord a => Judgement a -> Formula a -> Judgement a Source #

Weaken a judgement by inserting a formula into its hypotheses.

>>> weakenJudgement ([Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b') (Var 'c')
[Var 'a',Var 'c',Imp (Var 'a') (Var 'b')] |- Var 'b'

Proofs

data Proof a where Source #

A proof tree for propositional logic.

Bundled Patterns

pattern Axiom :: Judgement a -> Proof a	An axiom `(Axiom (g \|- a))` represents the inference of the judgement $g \vdash a$, where $a \in g$: \[ \frac{}{ g \vdash a } \, (\text{Axiom}) \]
pattern FalseElim :: Judgement a -> Proof a -> Proof a	Falsity elimination (principle of explosion). `(FalseElim (g \|- a) p)` represents the inference of the judgement $g \vdash a$ given a proof $p$ of $g \vdash \bot$: \[ \frac{ \displaystyle\frac{ p }{ g \vdash \bot } }{ g \vdash a } \, ({\bot}\text{E}) \]
pattern TrueIntr :: Judgement a -> Proof a	Truth introduction. `(TrueIntr (g \|- Lit True))` represents the vacuous inference of the judgement $g \vdash \top$: \[ \frac{}{ g \vdash \top } \, (\top\text{I}) \]
pattern NotElim :: Judgement a -> Proof a -> Proof a -> Proof a	Negation elimination. `(NotElim (g \|- Lit False) p q)` represents the inference of the judgement $g \vdash \bot$ given a proof $p$ of $g_1 \vdash \lnot a$ and a proof $q$ of $g_2 \vdash a$, where $g = g_1 \cup g_2$: \[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash \lnot a } \qquad \displaystyle\frac{ q }{ g_2 \vdash a } }{ g \vdash \bot } \, ({\lnot}\text{E}) \]
pattern NotIntr :: Judgement a -> Proof a -> Proof a	Negation introduction. `(NotIntr (g \|- (Not a)) p)` represents the inference of the judgement $g \vdash \lnot a$ given a proof $p$ of $g, a \vdash \bot$: \[ \frac{ \displaystyle\frac{ p }{ g, a \vdash \bot } }{ g \vdash \lnot a } \, ({\lnot}\text{I}) \]
pattern ImpElim :: Judgement a -> Proof a -> Proof a -> Proof a	Implication elimination (modus ponens). `(ImpElim (g \|- b) p q)` represents the inference of the judgement $g \vdash b$ given a proof $p$ of $g_1 \vdash a \rightarrow b$ and a proof $q$ of $g_2 \vdash a$, where $g = g_1 \cup g_2$: \[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \rightarrow b } \qquad \displaystyle\frac{ q }{ g_2 \vdash a } }{ g \vdash b } \, ({\rightarrow}\text{E}) \]
pattern ImpIntr :: Judgement a -> Proof a -> Proof a	Implication introduction. `(ImpIntr (g \|- (Imp a b) p)` represents the inference of the judgement $g \vdash a \rightarrow b$ given a proof $p$ of $g, a \vdash b$: \[ \frac{ \displaystyle\frac{ p }{ g, a \vdash b } }{ g \vdash a \rightarrow b } \, ({\rightarrow}\text{I}) \]
pattern OrElim :: Judgement a -> Proof a -> Proof a -> Proof a -> Proof a	Disjunction elimination. `(OrElim (g \|- c) p q r)` represents the inference of the judgement $g \vdash c$ given proofs $p$ of $g_1 \vdash a \lor b$, $q$ of $g_2, a \vdash c$, and $r$ of $g_3, b \vdash c$, where $g = g_1 \cup g_2 \cup g_3$: \[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \lor b } \qquad \displaystyle\frac{ q }{ g_2, a \vdash c } \qquad \displaystyle\frac{ r }{ g_3, b \vdash c } }{ g \vdash c } \, ({\lor}\text{E}) \]
pattern OrIntrL :: Judgement a -> Proof a -> Proof a	Left disjunction introduction. `(OrIntrL (g \|- (Or a b)) p)` represents the inference of the judgement $g \vdash a \lor b$ given a proof $p$ of $g \vdash a$: \[ \frac{ \displaystyle\frac{ p }{ g \vdash a } }{ g \vdash a \lor b } \, ({\lor}\text{IL}) \]
pattern OrIntrR :: Judgement a -> Proof a -> Proof a	Right disjunction introduction. `(OrIntrR (g \|- (Or a b)) p)` represents the inference of the judgement $g \vdash a \lor b$ given a proof $p$ of $g \vdash b$: \[ \frac{ \displaystyle\frac{ p }{ g \vdash b } }{ g \vdash a \lor b } \, ({\lor}\text{IR}) \]
pattern AndElimL :: Judgement a -> Proof a -> Proof a	Left conjunction elimination. `(AndElimL (g \|- a) p)` represents the inference of the judgement $g \vdash a$ given a proof $p$ of $g \vdash a \land b$: \[ \frac{ \displaystyle\frac{ p }{ g \vdash a \land b } }{ g \vdash a } \, ({\land}\text{EL}) \]
pattern AndElimR :: Judgement a -> Proof a -> Proof a	Right conjunction elimination. `(AndElimR (g \|- b) p)` represents the inference of the judgement $g \vdash b$ given a proof $p$ of $g \vdash a \land b$: \[ \frac{ \displaystyle\frac{ p }{ g \vdash a \land b } }{ g \vdash b } \, ({\land}\text{ER}) \]
pattern AndIntr :: Judgement a -> Proof a -> Proof a -> Proof a	Conjunction introduction. `(AndIntr (g \|- (And a b)) p)` represents the inference of the judgement $g \vdash a \land b$ given a proof $p$ of $g_1 \vdash a$ and a proof $q$ of $g_2 \vdash b$, where $g = g_1 \cup g_2$: \[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a } \qquad \displaystyle\frac{ q }{ g_2 \vdash b } }{ g \vdash a \land b } \, ({\land}\text{I}) \]
pattern IffElimL :: Judgement a -> Proof a -> Proof a	Left equivalence elimination. `(IffElimL (g \|- (Imp a b)) p)` represents the inference of the judgement $g \vdash a \rightarrow b$ given a proof $p$ of $g \vdash a \leftrightarrow b$: \[ \frac{ \displaystyle\frac{ p }{ g \vdash a \leftrightarrow b } }{ g \vdash a \rightarrow b } \, ({\leftrightarrow}\text{EL}) \]
pattern IffElimR :: Judgement a -> Proof a -> Proof a	Right equivalence elimination. `(IffElimR (g \|- (Imp b a)) p)` represents the inference of the judgement $g \vdash b \rightarrow a$ given a proof $p$ of $g \vdash a \leftrightarrow b$: \[ \frac{ \displaystyle\frac{ p }{ g \vdash a \leftrightarrow b } }{ g \vdash b \rightarrow a } \, ({\leftrightarrow}\text{ER}) \]
pattern IffIntr :: Judgement a -> Proof a -> Proof a -> Proof a	Equivalence introduction. `(IffIntr (g \|- (Iff a b)) p)` represents the inference of the judgement $g \vdash a \leftrightarrow b$ given a proof $p$ of $g_1 \vdash a \rightarrow b$ and a proof $q$ of $g_2 \vdash b \rightarrow a$, where $g = g_1 \cup g_2$: \[ \frac{ \displaystyle\frac{ p }{ g_1 \vdash a \rightarrow b } \qquad \displaystyle\frac{ q }{ g_2 \vdash b \rightarrow a } }{ g \vdash a \leftrightarrow b } \, ({\leftrightarrow}\text{I}) \]

Instances

Instances details

Eq a => Eq (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types Methods (==) :: Proof a -> Proof a -> Bool # (/=) :: Proof a -> Proof a -> Bool #
Ord a => Ord (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types Methods compare :: Proof a -> Proof a -> Ordering # (<) :: Proof a -> Proof a -> Bool # (<=) :: Proof a -> Proof a -> Bool # (>) :: Proof a -> Proof a -> Bool # (>=) :: Proof a -> Proof a -> Bool # max :: Proof a -> Proof a -> Proof a # min :: Proof a -> Proof a -> Proof a #
(Ord a, Read a) => Read (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types Methods readsPrec :: Int -> ReadS (Proof a) # readList :: ReadS [Proof a] # readPrec :: ReadPrec (Proof a) # readListPrec :: ReadPrec [Proof a] #
Show a => Show (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types Methods showsPrec :: Int -> Proof a -> ShowS # show :: Proof a -> String # showList :: [Proof a] -> ShowS #
AST (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types Associated Types type Root (Proof a) Source # Methods root :: Proof a -> Root (Proof a) Source # children :: Proof a -> [Proof a] Source # metadata :: Proof a -> ASTMetadata Source # height :: Proof a -> Int Source # size :: Proof a -> Int Source #
PrettyPrintable a => PrettyPrintable (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types Methods pretty :: Proof a -> String Source # prettys :: Proof a -> ShowS Source #
type Root (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types type Root (Proof a) = Judgement a

Provability checking

isProvable :: Ord a => Judgement a -> Bool Source #

Determine whether a judgement is classically valid.

Examples

Expand

>>> isProvable $ [Not (Not (Var 'a'))] |- Var 'a'
True

>>> isProvable $ [Var 'a'] |- Var 'b'
False

isTautology :: Ord a => Formula a -> Bool Source #

Determine whether a formula is a classically tautology.

Examples

Expand

>>> isTautology $ Or (Var 'a') (Not (Var 'a'))
True
>>> isTautology $ Var 'a'
False

Satisfiability

Truth assignments

class TruthAssignment t a where Source #

Class representing truth assignments for evalutating propositional logic formulas.

Minimal complete definition

evalVar

Methods

evalVar :: t -> a -> Bool Source #

Evaluate the truth value of a variable under a given truth assignment.

evalFormula :: t -> Formula a -> Bool Source #

Evaluate the truth value of a formula under a given truth assignment.

Instances

Instances details

TruthAssignment () a Source #	Assigns all propositional variables the truth value `False`. Can be used to evaluate closed formulas. Examples Expand `>>>` `() \|= (Var "a")`False `>>>` `() \|= (Or (Lit True) (Lit False))`True
Instance details Defined in AutoProof.Internal.Classical.SAT.TruthAssignment Methods evalVar :: () -> a -> Bool Source # evalFormula :: () -> Formula a -> Bool Source #
Ord a => TruthAssignment (Map a Bool) a Source #	Truth assignments where a missing key in the map is interpreted as `False`. Examples Expand `>>>` `t = Map.fromList $ [("a", True), ("b", False)]``>>>` `t \|= And (Var "a") (Not (Var "b"))`True `>>>` `t = Map.fromList $ [("a", True)]``>>>` `t \|= Imp (Var "a") (Var "b")`False
Instance details Defined in AutoProof.Internal.Classical.SAT.TruthAssignment Methods evalVar :: Map a Bool -> a -> Bool Source # evalFormula :: Map a Bool -> Formula a -> Bool Source #

(|=) :: TruthAssignment t a => t -> Formula a -> Bool infix 5 Source #

Semantic entailment relation. This is an infix alias of evalFormula.

Examples

Expand

>>> t = Map.fromList $ [("a", True), ("b", False)]
>>> t |= And (Var "a") (Not (Var "b"))
True

Check satisfiability

satSimple :: Eq a => Formula a -> Bool Source #

A simple baseline satisfiability algorithm.

This algorithm is based on the observation that if $a$ is a propositional formula and $x$ is a propositional variable, then $a$ is satisfiable if and only if either $a[\top/x]$ is satisfiable or $a[\bot/x]$ is satisfiable.

Examples

Expand

>>> satSimple $ Var "a"
True

>>> satSimple $ And (Var "a") (Not (Var "a"))
False

satDPLL :: Ord a => Formula a -> Bool Source #

DPLL satisfiability algorithm.

Examples

Expand

>>> import AutoProof.Internal.Formula
>>> satDPLL $ Var "a"
True

>>> satDPLL $ And (Var "a") (Not (Var "a"))
False

Satisfying assignment search

satAssignmentSimple :: Ord a => Formula a -> Maybe (Map a Bool) Source #

A simple baseline satisfiability algorithm, returning a satisfying truth assignment if there is one.

This algorithm is based on the observation that if $a$ is a propositional formula and $x$ is a propositional variable, then $a$ is satisfiable if and only if either $a[\top/x]$ is satisfiable or $a[\bot/x]$ is satisfiable.

Examples

Expand

>>> a = And (Not (Var "a")) (Or (Var "b") (Var "c")) -- satisfiable
>>> Just t = satAssignmentSimple a
>>> t
fromList [("a",False),("b",True),("c",True)]
>>> t |= a
True

>>> satAssignmentSimple $ And (Var "a") (Not (Var "a")) -- unsatisfiable
Nothing

satAssignmentDPLL :: Ord a => Formula a -> Maybe (Map a Bool) Source #

DPLL satisfiability algorithm, returning a satisfying truth assihnment, if there is one.

Examples

Expand

>>> a = And (Not (Var "a")) (Or (Var "b") (Var "c")) -- satisfiable
>>> Just t = satAssignmentDPLL a
>>> t
fromList [("a",False),("c",True)]
>>> t |= a
True

Note: The variable "b" is missing in the map above, which means that it's implictly assigned the value False.

>>> satAssignmentDPLL $ And (Var "a") (Not (Var "a")) -- unsatisfiable
Nothing

Abstract syntax trees

class AST t where Source #

Abstract syntax tree class.

Minimal complete definition

root, children, metadata

Associated Types

type Root t Source #

The type of the values annotating AST nodes.

Methods

root :: t -> Root t Source #

The value at the AST's root node.

children :: t -> [t] Source #

The AST's child ASTs.

height :: t -> Int Source #

Number of edges on the longest path from the root of the AST to a leaf.

size :: t -> Int Source #

Number of nodes in the AST.

Instances

Instances details

AST (Formula a) Source #
Instance details Defined in AutoProof.Internal.Formula.Types Associated Types type Root (Formula a) Source # Methods root :: Formula a -> Root (Formula a) Source # children :: Formula a -> [Formula a] Source # metadata :: Formula a -> ASTMetadata Source # height :: Formula a -> Int Source # size :: Formula a -> Int Source #
AST (Proof a) Source #
Instance details Defined in AutoProof.Internal.Proof.Types Associated Types type Root (Proof a) Source # Methods root :: Proof a -> Root (Proof a) Source # children :: Proof a -> [Proof a] Source # metadata :: Proof a -> ASTMetadata Source # height :: Proof a -> Int Source # size :: Proof a -> Int Source #

subtrees :: (AST t, Ord t) => t -> Set t Source #

(subtrees t) is the set of all subtrees of an AST t (including t itself).

properSubtrees :: (AST t, Ord t) => t -> Set t Source #

(properSubtrees t) is the the set of all proper subtrees of an AST t (i.e., not including t itself).

Parsing

parseFormula :: String -> Maybe (Formula String) Source #

(parseFormula s) parses a string s as a propositional formula, returning a Just a on success, where a is the parsed formula.

For a version of parseFormula that does not return a wrapped formula but also throws an error when it cannot parse, see unsafeParseFormula.

Conventions

Expand

Supported connective symbols:
- Negation: "~", "¬".
- Implication: "->", "=>", "→", "⇾", "⇒" "⊃".
- Disjunction: "|", "\/", "∨", "+"
- Conjunction: "&", "/\", "∧", "^", "*"
- Equivalence: "<->", "↔", "⇿", "⇔"
Implication is right-associative and has lower precedence than the other connectives.
Equivalence is left-associative and has higher precedence than implication but lower precedence than conjunction and disjunction.
Disjunction is left-associative and has higher precedence than equivalence but lower precedence than conjunction.
Conjunction is left-associative and has highest precedence out of the binary connectives.
Negation binds most tightly, and must immediately precede its argument (i.e., there should not be a space between a negation symbol and the proposition that follows).
Valid variable names begin with a letter (uppercase or lowercase) or an underscore, and may be followed by a letter, underscore, digit, or single quote (a "prime" symbol). The exceptions are the strings "false" and "true", which are parsed as the propositional literals $\bot$ and $\top$, respectively.

Examples

Expand

>>> parseFormula "a -> b -> c"
Just (Imp (Var "a") (Imp (Var "b") (Var "c")))

>>> parseFormula "~a | b -> c"
Just (Imp (Or (Not (Var "a")) (Var "b")) (Var "c"))

>>> parseFormula "(a -> b) & ~c"
Just (And (Imp (Var "a") (Var "b")) (Not (Var "c")))

parseJudgement :: String -> Maybe (Judgement String) Source #

(parseJudgement s) parses a string s as a propositional judgement.

A valid judgement is made up of an antecedent, a turnstile symbol, and a consequent (in that order). The antecedents are a (potentially empty) comma-separated list of formulas, the turnstile symbol is either "|-" or "⊢", and the consequent is another formula.

See parseFormula for the specification of valid formulas.

Examples

Expand

>>> parseJudgement "a, a -> b |- b"
Just ([Var "a",Imp (Var "a") (Var "b")] |- Var "b")

>>> parseJudgement "a |- a | b"
Just ([Var "a"] |- Or (Var "a") (Var "b"))

Pretty-printing

pretty :: PrettyPrintable a => a -> String Source #

Pretty-print a value.

prettyFormula :: PrettyPrintable a => Formula a -> String Source #

Get a pretty-printed representation of a propositional formula.

Examples

Expand

>>> prettyFormula $ Imp (Var "a") (Or (Var "b") (Lit False))
"a → (b ∨ ⊥)"

prettyJudgement :: PrettyPrintable a => Judgement a -> String Source #

Get a pretty-printed representation of a judgement.

Examples

Expand

>>> prettyJudgement $ [Var "a", Imp (Var "a") (Var "b")] |- Var "b"
"a, a → b ⊢ b"

prettyProof :: PrettyPrintable a => Proof a -> String Source #

Get a pretty-printed representation of a proof.