Proof Editor for Propositional Temporal Logic

摘要

This report describes propositional temporal logic (PTL), a program to assist in constructing proofs in propositional logic extended by the operators ('always',) ('eventually', and 'at the next step'). PTL is neither a proof generator nor a proof checker. Instead, it is a proof editor. It provides convenient commands to manipulate logical formulas in order to ease the task of constructing valid proofs. PTL is written in Zetalisp and runs on the Symbolics 3600 workstation. PTL is not a stand-alone program. It is a number of additional commands that extend the 3600 editor, Zmacs. All of the deduction rules of PTL are implemented.