FORMALIZATION OF PROPOSITIONAL LINEAR TEMPORAL LOGIC IN THE MIZAR SYSTEM
Selected contents from this journal
Languages of publication
The paper describes formalization of some issues of propositional linear temporal logic (PLTL). We discuss encountered problems and applied solutions. The formalization was carried out in the Mizar system. In comparison with other systems, Mizar is famous for its large repository of computer checked mathematical knowledge and also for its user-friendly knowledge representation and proof language.
Publication order reference
CEJSH db identifier