Authors: Cláudia Nalon and Dirk Pattinson
Paper Information
Title: | A Resolution-Based Calculus for Preferential Logics |
Authors: | Cláudia Nalon and Dirk Pattinson |
Proceedings: | IJCAR Proceedings 9th IJCAR, 2018 |
Editors: | Stephan Schulz, Didier Galmiche and Roberto Sebastiani |
Keywords: | Preferential Logics, Modal Logics, Resolution |
Abstract: | ABSTRACT. The vast majority of modal theorem provers implement modal tableau, or backwards proof search in (cut-free) sequent calculi. The design of suitable calculi is highly non-trivial, and employs nested sequents, labelled sequents and/or specifically designated transitional formulae. Theorem provers for first-order logic, on the other hand, are by and large based on resolution. In this paper, we present a resolution system for preference-based modal logics, specifically Burgess' system S. Our main technical results are soundness and completeness. Conceptually, we argue that resolution-based systems are not more difficult to design than cut-free sequent calculi but their purely syntactic nature makes them much better suited for implementation in automated reasoning systems. |
Pages: | 16 |
Talk: | Jul 15 09:00 (Session 101D: Logics and Calculi) |
Paper: |