Carregant...
Carregant...

Vés al contingut (premeu Retorn)

Invariant-free clausal temporal resolution

Autor
Gaintzarain, J.; Hermo, M.; Lucio, P.; Navarro, M.; Orejas, F.
Tipus d'activitat
Article en revista
Revista
Journal of automated reasoning
Data de publicació
2013-01
Volum
50
Número
1
Pàgina inicial
1
Pàgina final
49
DOI
https://doi.org/10.1007/s10817-011-9241-2 Obrir en finestra nova
Resum
Resolution is a well-known proof method for classical logics that is well suited for mechanization. The most fruitful approach in the literature on temporal logic, which was started with the seminal paper of M. Fisher, deals with Propositional Linear-time Temporal Logic (PLTL) and requires to generate invariants for performing resolution on eventualities. The methods and techniques developed in that approach have also been successfully adapted in order to obtain a clausal resolution method for C...
Paraules clau
Clausal normal form, Invariant-free, Propositional linear-time temporal logic, Resolution
Grup de recerca
ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals

Participants

  • Gaintzarain, Jose  (autor)
  • Hermo Huguet, Montserrat  (autor)
  • Lucio, Paqui  (autor)
  • Navarro Gómez, Marisa  (autor)
  • Orejas Valdes, Fernando  (autor)