Please use this identifier to cite or link to this item:
Title: On Herbrand’s Theorem for Hybrid Logic
Author: Costa, Diana
Martins, Manuel
Marcos, João
Issue Date: 1-Apr-2019
Publisher: Colege Publications
Abstract: The original version of Herbrand’s theorem [8] for first-order logic provided the theoretical underpinning for automated theorem proving, by allowing a constructive method for associating with each first-order formula χ a sequence of quantifier-free formulas χ1, χ2, χ3, · · · so that χ has a first-order proof if and only if some χi is a tautology. Some other versions of Herbrand’s theorem have been developed for classical logic, such as the one in [6], which states that a set of quantifier-free sentences is satisfiable if and only if it is propositionally satisfiable. The literature concerning versions of Herbrand’s theorem proved in the context of non-classical logics is meager. We aim to investigate in this paper two versions of Herbrand’s theorem for hybrid logic, which is an extension of modal logic that is expressive enough so as to allow identifying specific sates of the corresponding models, as well as describing the accessibility relation that connects these states, thus being completely suitable to deal with relational structures [3]. Our main results state that a set of satisfaction statements is satisfiable in a hybrid interpretation if and only if it is propositionally satisfiable
Peer review: yes
ISSN: 2055 3706
Appears in Collections:CIDMA - Artigos
AGG - Artigos

Files in This Item:
File Description SizeFormat 
Herbrand.pdf323.88 kBAdobe PDFView/Open

Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.