Document Open Access Logo

Linking Focusing and Resolution with Selection

Author Guillaume Burel

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2018.9.pdf
  • Filesize: 435 kB
  • 14 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Automated reasoning
Keywords
  • logic in computer science
  • automated deduction
  • proof theory
  • sequent calculus
  • refinements of resolution
  • deduction modulo theory
  • polarization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Focusing and selection are techniques that shrink the proof search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atom can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof search space.

Cite As Get BibTex

Guillaume Burel. Linking Focusing and Resolution with Selection. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.MFCS.2018.9

Author Details

Guillaume Burel
  • ENSIIE and Samovar, Télécom SudParis and CNRS, Université Paris-Saclay, Évry, France, Inria and LSV, CNRS and ENS Paris-Saclay, Université Paris-Saclay, Cachan, France

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. Google Scholar
  2. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):1-31, 1994. Google Scholar
  3. Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 19-99. Elsevier and MIT Press, 2001. Google Scholar
  4. Paul Brauner, Clément Houtmann, and Claude Kirchner. Principle of superdeduction. In Luke Ong, editor, LICS, pages 41-50, 2007. Google Scholar
  5. Guillaume Burel. Experimenting with deduction modulo. In Viorica Sofronie-Stokkermans and Nikolaj Bjørner, editors, CADE, volume 6803 of LNCS, pages 162-176. Springer, 2011. Google Scholar
  6. Guillaume Burel. From axioms to rewriting rules. Available on author’s web page, 2013. Google Scholar
  7. Guillaume Burel. Cut admissibility by saturation. In Gilles Dowek, editor, RTA-TLCA, volume 8560 of LNCS, pages 124-138. Springer, 2014. Google Scholar
  8. Guillaume Burel and Gilles Dowek. How can we prove that a proof search method is not an instance of another? In LFMTP, ACM International Conference Proceeding Series, pages 84-87. ACM, 2009. Google Scholar
  9. Guillaume Burel and Claude Kirchner. Regaining cut admissibility in deduction modulo using abstract completion. Information and Computation, 208(2):140-164, 2010. Google Scholar
  10. Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, and Olivier Hermant. Automated deduction in the B set theory using typed proof search and deduction modulo. In Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, editors, LPAR, volume 35 of EPiC Series in Computing, pages 42-58. EasyChair, 2015. Google Scholar
  11. Samuel R. Buss, editor. Handbook of proof theory. Studies in logic and the foundations of mathematics. Elsevier, Amsterdam, 1998. Google Scholar
  12. Kaustuv Chaudhuri and Frank Pfenning. A focusing inverse method theorem prover for first-order linear logic. In Robert Nieuwenhuis, editor, CADE, volume 3632 of LNCS, pages 69-83. Springer, 2005. Google Scholar
  13. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. Journal of Automated Reasoning, 40(2-3):133-177, 2008. Google Scholar
  14. Zakaria Chihani, Tomer Libal, and Giselle Reis. The proof certifier checkers. In TABLEAUX, volume 9323 of LNCS, pages 201-210, Wroclaw, Poland, 2015. Springer. Google Scholar
  15. Zakaria Chihani, Dale Miller, and Fabien Renaud. Foundational proof certificates in first-order logic. In Maria Paola Bonacina, editor, CADE, volume 7898 of LNCS, pages 162-177. Springer, 2013. Google Scholar
  16. Eric Deplagne and Claude Kirchner. Induction as deduction modulo. Rapport de recherche, LORIA, Nov 2004. URL: https://hal.inria.fr/LORIA/inria-00099871.
  17. Gilles Dowek. What is a theory? In Helmut Alt and Afonso Ferreira, editors, STACS, volume 2285 of LNCS, pages 50-64. Springer, 2002. Google Scholar
  18. Gilles Dowek. Truth values algebras and proof normalization. In Thorsten Altenkirch and Conor McBride, editors, TYPES, volume 4502 of LNCS, pages 110-124. Springer, 2006. Google Scholar
  19. Gilles Dowek. Polarized resolution modulo. In Cristian S. Calude and Vladimiro Sassone, editors, IFIP TCS, volume 323 of IFIP AICT, pages 182-196. Springer, 2010. Google Scholar
  20. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31(1):33-72, 2003. Google Scholar
  21. Gilles Dowek and Benjamin Werner. Proof normalization modulo. The Journal of Symbolic Logic, 68(4):1289-1316, 2003. Google Scholar
  22. Gilles Dowek and Benjamin Werner. Arithmetic as a theory modulo. In Jürgen Giesl, editor, RTA, volume 3467 of LNCS, pages 423-437. Springer, 2005. Google Scholar
  23. Mahfuza Farooque, Stéphane Graham-Lengrand, and Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. In Alberto Momigliano, Brigitte Pientka, and Randy Pollack, editors, LFMTP, pages 3-14. ACM, 2013. Google Scholar
  24. Olivier Hermant. Méthodes Sémantiques en Déduction Modulo. PhD thesis, École Polytechnique, 2005. Google Scholar
  25. Olivier Hermant. Resolution is cut-free. Journal of Automated Reasoning, 44(3):245-276, 2009. Google Scholar
  26. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi. Google Scholar
  27. Sean McLaughlin and Frank Pfenning. Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, LPAR, volume 5330 of Lecture Notes in Computer Science, pages 174-181. Springer, 2008. Google Scholar
  28. Dale Miller and Marco Volpe. Focused labeled proof systems for modal logic. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, LPAR, volume 9450 of LNCS, pages 266-280. Springer, 2015. Google Scholar
  29. J. A. Robinson. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 1:227-234, 1965. Google Scholar
  30. Peter Schroeder-Heister. Cut elimination for logics with definitional reflection. In Nonclassical Logics and Information Processing, volume 619 of LNCS, pages 146-171. Springer, 1990. Google Scholar
  31. James R. Slagle. Automatic theorem proving with renamable and semantic resolution. J. ACM, 14(4):687-697, 1967. Google Scholar
  32. Larry Wos, George A. Robinson, and Daniel F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. J. ACM, 12(4):536-541, 1965. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact