Chapter title | Tackling "until induction" in natural deduction for PLTL |
---|
Authors | Bolotov, A. |
---|
Abstract | 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. |
---|
Book title | Proceedings of the 15th workshop on automated reasoning: bridging the gap between theory and practice: CICM 2008, Conferences on Intelligent Computer Mathematics, University of Birmingham, UK |
---|
Year | 2008 |
---|
Publisher | School of Computer Science |
---|
Publication dates |
---|
Published | 2008 |
---|
Place of publication | Birmingham |
---|
Web address (URL) | http://www.csc.liv.ac.uk/~lad/arw08/bolotov-arw2008.pdf |
---|