{- | Module : $Header$

- Description : Implementation of the generic sequent calculus

- Copyright : (c) Daniel Hausmann & Lutz Schroeder, DFKI Lab Bremen,

- Rob Myers & Dirk Pattinson, Department of Computing, ICL

- License : GPLv2 or higher, see LICENSE.txt

- Maintainer : hausmann@dfki.de

- Stability : provisional

- Portability : portable

-

- Provides the implementation of the generic proving function.

- Also contains an optimized version of the proving function (using so-called

- 'memoizing')

-}

module GMP.Prover where

import Data.List

import Data.Ratio

import Data.Maybe

import Debug.Trace

import GMP.Logics.Generic

import GMP.Logics.K

{- ------------------------------------------------------------------------------

sequent calculus implementation

------------------------------------------------------------------------------ -}

{- Inference Rules

map a sequent to the list of all premises that derive

the sequent. Note that a premise is a list of sequents:

to prove Gamma, A /\ B we need both Gamma, A and Gamma, B as premises.

to prove Gamma, neg(A /\ B), we need Gamma, neg A, neg B as premise.

to prove A, neg A, Gamma we need no premises

So a premise is a list of sequents, and the list of all possible

premises therefore has type [[ Sequent ]] -}

{- the functions below compute the list of all possible premises

that allow to derive a given sequent using the rule that

lends its name to the function. -}

{- faster to check for atomic axioms

axiom1 xs = [ [] | p <- xs, (Not q) <- xs, p==q] -}

axiom_rule :: Sequent -> Premises

axiom_rule (Sequent xs) = [ [[Sequent ([] :: [Formula (K (K (K ())))])]] |

(Atom n) <- xs, (Neg (Atom m)) <- xs, m == n]

true_rule :: Sequent -> Premises

true_rule (Sequent xs) = [ [[Sequent ([] :: [Formula (K (K (K ())))])]] | T <- xs]

negfalse_rule :: Sequent -> Premises

negfalse_rule (Sequent xs) = [ [[Sequent ([] :: [Formula (K (K (K ())))])]] |

(Neg F) <- xs]

conj_rule :: Sequent -> Premises

conj_rule (Sequent as) = [ [[Sequent (p : delete f as)],

[Sequent (q : delete f as)]] | f@(And p q) <- as]

-- the rule for the modal operator

modal_rule :: [Bool] -> Sequent -> Premises

modal_rule flags (Sequent xs) = emptify (fMatch flags xs)

-- the rule for the modal operator - optimised version

omodal_rule :: [Bool] -> [Sequent] -> Sequent -> Premises

omodal_rule flags [Sequent ec] (Sequent xs) = emptify (fMatchOptimised flags xs [])

{- collect all possible premises, i.e. the union of the possible

premises taken over the set of all rules in one to get the

recursion off the ground. -}

{- CAVEAT: the order of axioms /rules has a HUGE impact on performance.

this is as good as it gets if we apply the individual rules

message for the afterworld: if youm want to find proofs quickly,

first look at the rules that induce branching.

we can do slightly better if we apply all rules that do not

induce branching in one single step. -}

allRules :: [Bool] -> Sequent -> Premises

allRules flags (Sequent seq) = let t = Sequent (expand seq)

axioms = axiom_rule t

trues = true_rule t

negfalses = negfalse_rule t

modals = modal_rule flags t

conjs = conj_rule t

in if flags !! 1 then

trace ("\n Axiom-rule: " ++ prettylll axioms ++

" True-rule: " ++ prettylll trues ++

" NegFalse-rule: " ++ prettylll negfalses ++

" Modal-rule: " ++ prettylll modals ++

" Conj-rule: " ++ prettylll conjs )

(axioms ++ trues ++ negfalses ++ conjs ++ modals)

else

axioms ++ trues ++ negfalses ++ conjs ++ modals

oallRules :: [Bool] -> [Sequent] -> Sequent -> Premises

oallRules flags ec (Sequent seq) = let t = Sequent (expand seq)

axioms = axiom_rule t

trues = true_rule t

negfalses = negfalse_rule t

modals = omodal_rule flags ec t

conjs = conj_rule t

in trace

("\n Axiom-rule: " ++ prettylll axioms ++

" True-rule: " ++ prettylll trues ++

" NegFalse-rule: " ++ prettylll negfalses ++

" Modal-rule: " ++ prettylll modals ++

" Conj-rule: " ++ prettylll conjs )

(axioms ++ trues ++ negfalses ++ conjs ++ modals)

{- A sequent is provable iff there exists a set of premises that

prove the sequent such that all elements in the list of premises are

themselves provable. -}

sprovable :: [Bool] -> Sequent -> Bool

sprovable flags (Sequent []) = True

sprovable flags (Sequent seq) = if flags !! 1 then

trace ("\n <Current Sequent:> " ++ pretty_seq (Sequent (expand seq))) $

any (all (any (sprovable flags))) (allRules flags (Sequent seq))

else any (all (any (sprovable flags))) (allRules flags (Sequent seq))

-- optimized, alla

osprovable :: [Bool] -> [Sequent] -> Sequent -> Bool

osprovable flags ec (Sequent []) = True

osprovable flags ec (Sequent seq) =

trace ("\n <Current Sequent:> " ++ pretty_seq (Sequent (expand seq))) $

any (all (any (osprovable flags ec))) (oallRules flags ec (Sequent seq))

-- specialisation to formulae

provable :: (SigFeature a b (c d), Eq (a (b (c d)))) => Formula (a (b (c d))) -> [Bool] -> Bool

provable phi flags = sprovable flags (Sequent [phi])

oprovable :: (SigFeature a b (c d), Eq (a (b (c d)))) => [Bool] -> [Sequent] -> Formula (a (b (c d))) -> Bool

oprovable flags ec phi = osprovable flags ec (Sequent [phi])

-- a formula is satisfiable iff it's negation is not provable

satisfiable :: (SigFeature a b (c d), Eq (a (b (c d)))) => Formula (a (b (c d))) -> [Bool] -> Bool

satisfiable phi flags = not (provable (neg phi) flags)

osatisfiable :: (SigFeature a b (c d), Eq (a (b (c d)))) => [Bool] -> [Sequent] -> Formula (a (b (c d))) -> Bool

osatisfiable flags ec phi = not (oprovable flags ec (neg phi))