Nonclausal resolution system for branching temporal logic

Nonclausal resolution system for branching temporal logic

Jurate Sakalauskaite

In 6th NWPT, pages 348-358

Abstract:

We present a proof system for branching propositional temporal logic. The system is based on nonclausal resolution.

The system is proved to be complete. The proof of completeness uses tableau construction for the logic

Comments
Institute of Mathematics and Informatics, Akademijos 4, 2600 Vilnius, Lithuania.

Available as PostScript, DVI.

[BRICS symbol] BRICS WWW home page