Terminating calculi for propositional Dummett logic with subformula property

DOI10.1007/S10817-013-9276-7MaRDI QIDQ2352485zbMATH OpenOpenAlexFDO

Authors Guido Fiorino

Publication date 2 July 2015

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.4458

zbMATH Keywords

automated theorem provingDummett logicsubformula propertytableau calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Intermediate logics (03B55)

Abstract: In this paper we present two terminating tableau calculi for propositional Dummett logic obeying the subformula property. The ideas of our calculi rely on the linearly ordered Kripke semantics of Dummett logic. The first calculus works on two semantical levels: the present and the next possible world. The second calculus employs the usual object language of tableau systems and exploits a property of the construction of the completeness theorem to introduce a check which is an alternative to loop check mechanisms.

Recommendations

• scientific article; zbMATH DE number 1361525
• An O(n n)-SPACE decision procedure for the propositional Dummett logic
• scientific article; zbMATH DE number 1612545
• Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus
• A deterministic terminating sequent calculus for Godel-Dummett logic

Cites work

• A deterministic terminating sequent calculus for Godel-Dummett logic
• A logic characterized by the class of connected models with nested domains
• A new algorithm for derivability in the constructive propositional calculus
• A propositional calculus with denumerable matrix
• Algebraic Completeness Results for Dummett's LC and Its Extensions
• An O(n n)-SPACE decision procedure for the propositional Dummett logic
• Computer Science Logic
• Decomposition proof systems for Gödel-Dummett logics
• Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics
• Graph-based decision for Gödel-Dummett logics
• scientific article; zbMATH DE number 1003731 (Why is no real title available?)
• scientific article; zbMATH DE number 1341466 (Why is no real title available?)
• scientific article; zbMATH DE number 6296791 (Why is no real title available?)
• Hypersequent Calculi for Godel Logics -- a Survey
• Making fuzzy description logic more general
• Metamathematics of fuzzy logic
• On the completenes principle: A study of provability in heyting's arithmetic and extensions

Cited in

(7)

• SAT-based proof search in intermediate propositional logics
• A deterministic terminating sequent calculus for Godel-Dummett logic
• scientific article; zbMATH DE number 1950257 (Why is no real title available?)
• From the subformula property to cut-admissibility in propositional sequent calculi
• scientific article; zbMATH DE number 2118592 (Why is no real title available?)
• An O(n n)-SPACE decision procedure for the propositional Dummett logic
• Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus

This page was built for publication: Terminating calculi for propositional Dummett logic with subformula property

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2352485)