FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A Resolution-Based Calculus for Preferential Logics

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: