Advertisement

Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic

  • Dominique Larchey-Wendling
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alessendro Avellone, Mauro Ferrari, and Pierangelo Miglioli. Duplication-Free Tableau Calculi and Related Cut-Free Sequent Calculi for the Interpolable Propositional Intermediate Logics. Logic Journal of the IGPL, 7(4):447–480, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 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. 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
  4. 4.
    Michael Dummett. A Propositional Calculus with a Denumerable matrix. Journal of Symbolic Logic, 24:96–107, 1959.MathSciNetGoogle Scholar
  5. 5.
    Roy Dyckhoff. Contraction-free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic, 57(3):795–807, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Roy Dyckhoff. A Deterministic Terminating Sequent Calculus for Gödel-Dummett logic. Logical Journal of the IGPL, 7:319–326, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 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. 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. 9.
    Kurt Gödel. Zum intuitionistischen Aussagenkalkül. Ergeb. Math. Koll, 4:40, 1933.Google Scholar
  10. 10.
    P. Hajek. Metamathematics of Fuzzy Logic. Kluwer Academic Publishers, 1998.Google Scholar
  11. 11.
    Jörg Hudelmaier. An O(n log n)-space decision procedure for Intuitionistic Propositional Logic. Journal of Logic and Computation, 3(1):63–75, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 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
  13. 13.
    O. Sonobe. A Gentzen-type Formulation of Some Intermediate Propositional Logics. Journal of Tsuda College, 7:7–14, 1975.MathSciNetGoogle Scholar
  14. 14.
    A. Visser. On the Completeness Principle: A study of provability in Heyting’s arithmetic. Annals of Mathematical Logic, 22:263–295, 1982.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Dominique Larchey-Wendling
    • 1
  1. 1.LORIAUniversité Henri PoincaréVandœuvre-lés-NancyFrance

Personalised recommendations