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.
A decision procedure for Propositional Dummett Logic was discussed. A tableau logic calculus for the logic was presented. The depth of the deductions was linearly bounded by the length of formulas to be proved in the procedure. Some theorems were discussed which were proved by using the semantic technique. The decision procedure was applied in computational space analysis.
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
A decision procedure for Propositional Dummett Logic was discussed. A tableau logic calculus for the logic was presented. The depth of the deductions was linearly bounded by the length of formulas to be proved in the procedure. Some theorems were discussed which were proved by using the semantic technique. The decision procedure was applied in computational space analysis.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
