Por Bruno Dinis (Universidade de Évora).

In this talk I introduce an extension of Hybrid Logic, dubbed VHL, in which quantifier domains (over world and domain variables) may vary from world to world. Relying on a novel notion of prenex form, it is possible to introduce a new form of Skolemization, which is a non-trivial refinement of the usual process. These concepts are strongly dependent on the @ operator, and are therefore referred to as @-prenex normal form, and @-Skolemization.

I give an overview of the steps necessary to prove a Herbrand-like theorem for VHL, stating the equivalence between the satisfiability of a set of formulas and the propositional satisfiability of the ground instances of an @-Skolemized version of these formulas.
(joint work with Diana Costa)

Transmissão via Zoom.