In this paper we present a new tableau calculus for propo- sitional Intuitionistic Logic in which the depth of the deductions is lin- early bounded in the length of the formula to be proved and giving rise to a O(n log n)-SPACE decision procedure. Soundness and completeness theorems are proved by a model-theoretic technique based on Kripke se- mantics of propositional Intuitionistic Logic. A sequent calculus giving rise a decision procedure with the same computational complexity has been given by Hudelmaier; such a calculus uses some specialized rules to treat sequents of a certain kind. Our calculus has both less rules and a narrower search space than Hudelmaier’s one. For this calculus we have an implementation.
Avellone, A., Fiorino, G., Moscato, U. (2004). A new a O(n log n)-SPACE decision procedure for propositional intuitionistic logic. In Collegium Logicum, Kurt Goedel Society (pp. 17-33). Vienna : KGS.
A new a O(n log n)-SPACE decision procedure for propositional intuitionistic logic
AVELLONE, ALESSANDRO;FIORINO, GUIDO GIUSEPPE;MOSCATO, UGO EMANUELE
2004
Abstract
In this paper we present a new tableau calculus for propo- sitional Intuitionistic Logic in which the depth of the deductions is lin- early bounded in the length of the formula to be proved and giving rise to a O(n log n)-SPACE decision procedure. Soundness and completeness theorems are proved by a model-theoretic technique based on Kripke se- mantics of propositional Intuitionistic Logic. A sequent calculus giving rise a decision procedure with the same computational complexity has been given by Hudelmaier; such a calculus uses some specialized rules to treat sequents of a certain kind. Our calculus has both less rules and a narrower search space than Hudelmaier’s one. For this calculus we have an implementation.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
