Tackling ”until induction” in natural deduction for PLTL

Bolotov, Alexander (2008) Tackling ”until induction” in natural deduction for PLTL. In: Dennis, L.A. and Sorge, V., (eds.) Proceedings of the automated reasoning workshop 2008. University of Birmingham, pp. 12-13.

Full text not available from this repository.

Official URL: http://events.cs.bham.ac.uk/cicm08/workshop-proc/a...


We investigate the problem of induction in the natural deduction construction of propositional linear-time temporal logic. The well known induction with the “always in the future” operator has been an obstacle in our previous developments of the proof search. Here we modify the formulation of the calculus by introducing new rules to deal with the “until” operator, show the correctness of a modified system and define proof search strategies for new rules based upon fixpoint characterisation of the Until operator.

Item Type:Book Section
Research Community:University of Westminster > Electronics and Computer Science, School of
ID Code:10957
Deposited On:27 Jul 2012 12:33
Last Modified:27 Jul 2012 12:33

Repository Staff Only: item control page