A Resolution-Based Calculus for Preferential Logics

Date

2018

Authors

Nalon, Cláudia
Pattinson, Dirk

Journal Title

Journal ISSN

Volume Title

Publisher

Springer Verlag

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 Open image in new window. 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.

Description

Keywords

Citation

Source

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Type

Conference paper

Book Title

Entity type

Access Statement

License Rights

Restricted until

2099-12-31

Downloads