Automating natural deduction for temporal logic

Bolotov, Alexander, Grigoriev, Oleg and Shangin, Vasilyi (2008) Automating natural deduction for temporal logic. In: Proceedings of the 14th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, ARW 2007. Imperial College, London.

Full text not available from this repository.
Official URL:


We present our recent work on the construction of natural deduction calculi for temporal logic. We analyse propositional linear-time temporal logic (PLTL) and Computation Tree Logic (CTL) and corresponding proof searching algorithms. The automation of the natural deduction calculi for these temporal logics opens the new prospect to apply our techniques as an automatic reasoning tool in the areas, where the linear-time or branching-time setting is required.

Item Type: Book Section
Uncontrolled Keywords: Automated deduction, temporal logic, natural deduction, proof search
Subjects: University of Westminster > Science and Technology > Electronics and Computer Science, School of (No longer in use)
Depositing User: Miss Nina Watts
Date Deposited: 22 Jan 2009 16:39
Last Modified: 14 Oct 2009 09:14

Actions (login required)

Edit Item (Repository staff only) Edit Item (Repository staff only)