Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic
- 296 Downloads
We present an algorithm for deciding Gödel-Dummett logic. The originality of this algorithm comes from the combination of proof-search in sequent calculus, which reduces a sequent to a set of pseudo-atomic sequents, and counter-model construction of such pseudo-atomic sequents by a fixpoint computation. From an analysis of this construction, we deduce a new logical rule [⊃ N ] which provides shorter proofs than the rule [⊃ R ] of G4-LC. We also present a linear implementation of the counter-model generation algorithm for pseudo-atomic sequents.
Unable to display preview. Download preview PDF.
- 2.Arnon Avron. A Tableau System for Gödel-Dummett Logic Based on a Hyper-sequent Calculus. In Roy Dyckhoff, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 1847 of Lecture Notes in Artificial Intelligence, pages 98–111, St Andrews, Scotland, July 2000.Google Scholar
- 3.L. Peter Deutsch and Daniel G. Bobrow. A Efficient Incremental Automatic Garbage Collector. Communications of the ACM, 19(9):522–526, September 1976.Google Scholar
- 7.Fiorino. An O(n log n)-SPACE decision procedure for the propositional Dummett Logic. to appear in Journal of Automated Reasoning.Google Scholar
- 8.Didier Galmiche and Dominique Larchey-Wendling. Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic. In Asian Computing Science Conference, ASIAN’99, volume 1742 of Lecture Notes in Computer Science, pages 101–102, Phuket, Thaïland, December 1999.Google Scholar
- 9.Kurt Gödel. Zum intuitionistischen Aussagenkalkül. Ergeb. Math. Koll, 4:40, 1933.Google Scholar
- 10.P. Hajek. Metamathematics of Fuzzy Logic. Kluwer Academic Publishers, 1998.Google Scholar
- 12.Dominique Larchey, Daniel Méry, and Didier Galmiche. STRIP: Structural Sharing for efficient Proof-Search. In International Joint Conference on Automated Reasoning, IJCAR 2001, volume 2083 of Lecture Notes in Artificial Intelligence, pages 696–700, Siena, Italy, January 2001.Google Scholar
- 15.Klaus Weich. Decisions Procedures for Intuitionistic Logic by Program Extraction. In International Conference TABLEAUX’98, volume 1397 of Lecture Notes in Artificial Intelligence, pages 292–306, Oisterwijk, The Netherlands, May 1998.Google Scholar