nkt — a prover for temporal logic
Countermodels and derivations in Volpe's labeled natural deduction systems N(Kt), N(Kl) and their extensions. Write a sequent, choose a system, and run it in SWI-Tinker.
insert:
Premisses separated by commas, then ⊢ and a labeled conclusion. ASCII also works:
~ & | => # |-.How to read the answer
The prover first builds a countermodel tree (unsigned, in the style of Jeffrey and Copeland). An open branch gives a countermodel, which is checked, and then no derivation exists. If the tree closes, the prover searches for a derivation in Volpe's system and checks it. In SWI-Tinker, press Ctrl-M to see the derivation as a tree and in Fitch style; the countermodel tree is given as qtree source.
| system | conditions on < |
|---|---|
| Kt | none (Lemmon's minimal tense logic) |
| K4t | transitive |
| Kl | transitive and connected: linear time (Volpe's N(Kl)) |
| Lin.Q | linear, without first or last instant, dense: the logic of the rationals |
The three extra conditions can be added to any system; they are independent and compatible.