Please use this identifier to cite or link to this item:
|Title:||On Herbrand’s Theorem for Hybrid Logic|
|Abstract:||The original version of Herbrand’s theorem  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 , 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 . Our main results state that a set of satisfaction statements is satisfiable in a hybrid interpretation if and only if it is propositionally satisfiable|
|Appears in Collections:||CIDMA - Artigos|
AGG - Artigos
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.