Document

# Linking Focusing and Resolution with Selection

## File

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

## Cite As

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

## 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.

## 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

## References

1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992.
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.
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.
4. Paul Brauner, Clément Houtmann, and Claude Kirchner. Principle of superdeduction. In Luke Ong, editor, LICS, pages 41-50, 2007.
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.
6. Guillaume Burel. From axioms to rewriting rules. Available on author’s web page, 2013.
7. Guillaume Burel. Cut admissibility by saturation. In Gilles Dowek, editor, RTA-TLCA, volume 8560 of LNCS, pages 124-138. Springer, 2014.
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.
9. Guillaume Burel and Claude Kirchner. Regaining cut admissibility in deduction modulo using abstract completion. Information and Computation, 208(2):140-164, 2010.
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.
11. Samuel R. Buss, editor. Handbook of proof theory. Studies in logic and the foundations of mathematics. Elsevier, Amsterdam, 1998.
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.
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.
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.
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.
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.
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.
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.
20. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31(1):33-72, 2003.
21. Gilles Dowek and Benjamin Werner. Proof normalization modulo. The Journal of Symbolic Logic, 68(4):1289-1316, 2003.
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.
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.
24. Olivier Hermant. Méthodes Sémantiques en Déduction Modulo. PhD thesis, École Polytechnique, 2005.
25. Olivier Hermant. Resolution is cut-free. Journal of Automated Reasoning, 44(3):245-276, 2009.
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.
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.
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.
29. J. A. Robinson. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 1:227-234, 1965.
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.
31. James R. Slagle. Automatic theorem proving with renamable and semantic resolution. J. ACM, 14(4):687-697, 1967.
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.