Nalon, CláudiaPattinson, DirkSebastiani, RGalmiche, DSchulz, S2024-02-12July 14-17978-331994204-9http://hdl.handle.net/1885/313385The 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.application/pdfen-AU© Springer International Publishing AG, part of Springer Nature 2018201810.1007/978-3-319-94205-6_332022-10-02