SimpleTheoremProver

Documentation

data Rule a

Based on https://bor0.wordpress.com/2018/08/07/simple-theorem-prover-in-racket/.

A rule is a way to change a theorem.

Constructors

Rule

Fields

• name :: String
• function :: a -> a

Instances

Show (Rule a)

Defined in SimpleTheoremProver

Methods

showsPrec :: Int -> Rule a -> ShowS

show :: Rule a -> String

showList :: [Rule a] -> ShowS

data Theorem a

A theorem is consisted of an initial axiom and rules (ordered set) applied

Constructors

Theorem

Fields

• axiom :: a
• rulesThm :: [Rule a]
• result :: a

Instances

Show a => Show (Theorem a)

Defined in SimpleTheoremProver

Methods

showsPrec :: Int -> Theorem a -> ShowS

show :: Theorem a -> String

showList :: [Theorem a] -> ShowS

data TheoremProver a

A prover system is consisted of a bunch of axioms and rules to apply between them

Constructors

TheoremProver

Fields

• axioms :: [Theorem a]
• rulesThmProver :: [Rule a]

Instances

Show a => Show (TheoremProver a)

Defined in SimpleTheoremProver

Methods

showsPrec :: Int -> TheoremProver a -> ShowS

show :: TheoremProver a -> String

showList :: [TheoremProver a] -> ShowS

mkAxiom :: a -> Theorem a

An axiom is just a theorem already proven

thmApplyRule :: Theorem a -> Rule a -> Theorem a

Applies a single rule to a theorem

thmApplyRules :: TheoremProver a -> [Theorem a] -> [Theorem a]

Applies all prover's rules to a list of theorems

mergeProofs :: Eq a => [Theorem a] -> [Theorem a] -> [Theorem a]

Merge two list of proofs but skip duplicate proofs, giving the first argument priority This is used to avoid circular results in the search tree E.g. application of rules resulting in an earlier theorem/axiom

findProofIter :: (Ord a, Eq a) => TheoremProver a -> a -> Int -> [Theorem a] -> Maybe (Theorem a)

Finds a proof by constructing a proof tree by iteratively applying theorem rules

findProof :: Ord a => TheoremProver a -> a -> Int -> Maybe (Theorem a)

Find proof helper