In this paper we provide the first (as far as we know) direct calculus deciding satisfiability of formulae in negation normal form in the fragment of hybrid logic with the satisfaction operator and the binder, where no occurrence of the $\Box$ operator is in the scope of a binder. A preprocessing step, rewriting formulae into equisatisfiable ones, turns the calculus into a satisfiability decision procedure for the fragment \mbox{$\Hl(@,\binder)$} $\setminus\Box \binder\Box$, {\ie} formulae in negation normal form where no occurrence of the binder is both in the scope of and contains in its scope a $\Box$ operator. The calculus is based on tableaux, where nominal equalities are treated by means of substitution, and termination is achieved by means of a form of anywhere blocking with indirect blocking. Direct blocking is a relation between nodes in a tableau branch, holding whenever the respective labels (formulae) are equal up to (a proper form of) nominal renaming. Indirect blocking is based on a partial order on the nodes of a tableau branch, which arranges them into a tree-like structure.

Cerrito, S., Cialdea, M. (2011). A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders. In Automated Reasoning with Analytic Tableaux and Related Methods (pp.104-118). BERLIN, HEIDELBERG : Springer [10.1007/978-3-642-22119-4_10].

A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders

CIALDEA, Marta
2011-01-01

Abstract

In this paper we provide the first (as far as we know) direct calculus deciding satisfiability of formulae in negation normal form in the fragment of hybrid logic with the satisfaction operator and the binder, where no occurrence of the $\Box$ operator is in the scope of a binder. A preprocessing step, rewriting formulae into equisatisfiable ones, turns the calculus into a satisfiability decision procedure for the fragment \mbox{$\Hl(@,\binder)$} $\setminus\Box \binder\Box$, {\ie} formulae in negation normal form where no occurrence of the binder is both in the scope of and contains in its scope a $\Box$ operator. The calculus is based on tableaux, where nominal equalities are treated by means of substitution, and termination is achieved by means of a form of anywhere blocking with indirect blocking. Direct blocking is a relation between nodes in a tableau branch, holding whenever the respective labels (formulae) are equal up to (a proper form of) nominal renaming. Indirect blocking is based on a partial order on the nodes of a tableau branch, which arranges them into a tree-like structure.
978-3-642-22118-7
Cerrito, S., Cialdea, M. (2011). A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders. In Automated Reasoning with Analytic Tableaux and Related Methods (pp.104-118). BERLIN, HEIDELBERG : Springer [10.1007/978-3-642-22119-4_10].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11590/178051
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 6
social impact