We prove ExpTime-membership of the satisfiability problem for loosely ∀-guarded first-order formulas with a bounded number of variables and an unbounded number of constants. Guarded fragments with constants are interesting by themselves and because of their connection to hybrid logic.
Guarded fragments with constants
FRANCESCHET, Massimo;
2005-01-01
Abstract
We prove ExpTime-membership of the satisfiability problem for loosely ∀-guarded first-order formulas with a bounded number of variables and an unbounded number of constants. Guarded fragments with constants are interesting by themselves and because of their connection to hybrid logic.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
jlli.pdf
non disponibili
Tipologia:
Altro materiale allegato
Licenza:
Non pubblico
Dimensione
151.55 kB
Formato
Adobe PDF
|
151.55 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.