The Properties of Sets of Temporal Logic Subformulas
This is a second preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [17]. We introduce two modified definitions of a subformula. In the former one we trea...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2012-12-01
|
| Series: | Formalized Mathematics |
| Online Access: | https://doi.org/10.2478/v10037-012-0026-9 |
| Summary: | This is a second preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [17]. We introduce two modified definitions of a subformula. In the former one we treat until-formula as indivisible. In the latter one, we extend the set of subformulas of until-formulas by a special disjunctive formula. This is needed to construct a temporal model. We also define an ordered positive-negative pair of finite sequences of formulas (PNP). PNPs represent states of a temporal model. |
|---|---|
| ISSN: | 1426-2630 1898-9934 |