Sciweavers

Share
CADE
2007
Springer

Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4

12 years 3 days ago
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4
We present a multi-context focused sequent calculus whose derivations are in bijective correspondence with normal natural deductions in the propositional fragment of the intuitionistic modal logic IS4. This calculus, suitable for the enumeration of normal proofs, is the starting point for the development of a sequent calculus-based bidirectional decision procedure for propositional IS4. In this system, relevant derived inference rules are constructed in a forward direction prior to proof search, while derivations constructed using these derived rules are searched over in a backward direction. We also present a variant which searches directly over normal natural deductions. Experimental results show that on most problems, the bidirectional prover is competitive with both conventional backward provers using loop-detection and inverse method provers, significantly outperforming them in a number of cases.
Samuli Heilala, Brigitte Pientka
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Samuli Heilala, Brigitte Pientka
Comments (0)
books