We present a tableau calculus for propositional Dummett Logic, also known as LC (\c{Linear Chain}), where the depth of the deductions are linearly bounded by the length of the formulas to be proved. We then show that it is possible to decide propositional Dummett Logic in \pspace.
Fiorino, G. (2001). An O(n log n)-SPACE decision procedure for the propositional Dummett Logic. JOURNAL OF AUTOMATED REASONING, 27(3), 297-311 [10.1023/A:1017515831550].
An O(n log n)-SPACE decision procedure for the propositional Dummett Logic
FIORINO, GUIDO GIUSEPPE
2001
Abstract
We present a tableau calculus for propositional Dummett Logic, also known as LC (\c{Linear Chain}), where the depth of the deductions are linearly bounded by the length of the formulas to be proved. We then show that it is possible to decide propositional Dummett Logic in \pspace.
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.
