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.
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)|