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.
Capitolo o saggio
complexity, decision procedure, proof theory
English
Collegium Logicum, Kurt Goedel Society
2004
3-901546-03-0
KGS
17
33
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.
none
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/357
Citazioni
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
Social impact