Table of Contents

• 1. The main Function
  • 1.1. REPL
• 2. Formulas
• 3. Canonical Representation of Formulas
• 4. Propositional Theorem Prover
• 5. Modal Theorem Prover
  • 5.1. proveK

This purpose of this project is to develop an efficient and modular theorem prover for modal logic. Recent work in modal logic has revealed proof theoretic structures that are flexible and versatile. This project focuses on tree hypersequents. A tree hypersequent is a tree whose nodes are sequents. A sequent is an ordered pair of sets of formulas. Sequents have recently enjoyed more attention in philosophical and proof theoretic circles because of their versatility. Tree hypersequents can be used to represent most standard Kripkean modal systems. This is a result from Francesca Poggiolesi

@INCOLLECTION{Poggiolesi_TMTHFMPL_2009,
  AUTHOR={Francesca Poggiolesi},
  TITLE={The Method of Tree-Hypersequents for Modal Propositional Logic},
  BOOKTITLE={Towards Mathematical Philosophy},
  YEAR={2009},
  PUBLISHER={Springer},
  PAGES={31--51},
  VOLUME={28}
}

The different modal systems, e.g. system T and system K, are represented by different structural rules that can be applied to the trees. But, for each system the rules that govern formulas, e.g. Left Negation and Right Necessity, are the same for each system. This means that a modal theorem prover that uses them is modular – we only need to change structural rules the core theorem prover is the same throughout.

The main Function

We've written tests for a couple of the main features of the theorem prover. The main function runs all the tests in a verbose mode. For now, the theorem prover is meant to be used with a REPL, so different functions can be called and tested. When the guts of the theorem prover are done, we will use the main function to generate an interface for the user to decide which system they would like to use and input a formula to prove. It might also be nice to ask for an expected result and add that to our test cases.

REPL

In order to use all of the functions, open up a REPL with GHC (or any other Haskell REPL):

andrew@Gentzen:~/Documents/haskell/modal-theorem-prover$ ghci
 GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
  Prelude>

Once there you can use :load DepthFirstTheoremProver.hs to load of the file. Then you'll have access to any function defined in DepthFirstTheoremProver.hs

Formulas

We take advantage of Haskell's strong typing to generate a Formula type. The type consistions of atomic formulas, negations, implications, conjunctions, disjunctions, possibilities, and necessities:

• AtomicFormula: a function from a string to an atomic formula, e.g. (AtomicFormula "The ground is wet")
• Not: a function from a Formula to a Formula, e.g. (Not (AtomicFormula "It is Raining"))
• Implies: a function from two formulas to a Formula, e.g. (Implies (AtomicFormula "Penny is dog") (AtomicFormula "Penny is a mammal"))
• And: a function from a list of formulas to a Formula, e.g. (And [(AtomicFormula "p"), (Not (AtomicFormula "p"))]) – a contradiction
• Or: a function form a list of formulas to a Formula, e..g (Or [(AtomicFormula "p"), (Not (AtomicFormula "p"))]) – a tautology (Sorry! I made this classical instead of constructive because constructive modal logic is not really well explored. When I get the chance to do some research into intuitionistic modal logics, I'll write that theorem prover.)
• Possibly: A function from a Formula to a Formula, e.g. (Possibly (AtomicFormula "it is raining"))
• Necessarily: A function from a Formula to a Formula, e.g. (Necessarily (Implies (AtomicFormula "A is a square") (AtomicFormula "A has four sides")))

Canonical Representation of Formulas

This function is responsible for removing all implications from formulas, pushing negations in as far as they can go, and ordering conjuncts and disjuncts in a canonical way. Ideally it would organize a formula in a way that is optimizes the therorem prover. We do not use Disjunctive Normal Form (DNF) for the formulas because we found empirically that it was slower. I think this is explained by the fact that a classical two sided sequent system is a way of making DNFs. So we end up redoing work in a much more complicated way if we convert a formula to DNF and then run it through the theorem prover.

Propositional Theorem Prover

Since we needed the classical propositional rules for a logic, and because it's better for testing, we added a propositional theorem prover. The main entry point to this functionality is the function propositionalProve :: Formula -> Bool. To use this function at the REPL call propositionalProve of a Formula e.g.

*Main> propositionalProve (Implies (Implies (Implies (AtomicFormula "p") (AtomicFormula "q")) (AtomicFormula "p")) (AtomicFormula "p"))
True

Modal Theorem Prover

Currently we only support proofs in System K. That's going to be updated soon with proofs from other modal systems. The cool thing about Tree Hypersequents is that you only really need on modal theorem prover – the prover for system K. All of the rules for manipulating formulas themselves are the same throughout the various systems.

proveK

The primary interface for proving formulas in System K is proveK. Here's an example:

*Main> proveK (Implies (Necessarily (Implies (AtomicFormula "p") (AtomicFormula "q"))) (Implies (Necessarily (AtomicFormula "p")) (Necessarily (AtomicFormula "q"))))
True

Footnotes:

¹ In my dissertation (see [my website](https://andrewparisi.weebly.com/research.html)) I develop a proof system for modal logics that only uses lists of sequents as opposed to trees of sequents as the primary proof object. These are known as hypersequents. This project spun off of another one with some friends to develop a automated theorem prover for hypersequents. I had some questions as to whether hypersequents or tree hypersequents would be a more effective proof object when it comes to automated theorem proving. For more information about that project email me at [[email protected]]([email protected]).

² A point of interesting reasearch is whether this is actually better. I think we might actually get an efficiency gain by changing the way that different modal universal rules (i.e. (Necessarily P) when true, and (Possibly P) when false) work when we have different systems. This is worth exploring for both hypersequents and tree hypersequents.