Reseña: Formalization of propositional linear temporal logic in the Mizar system

PorJosé A. Alonso

Una línea de trabajo dentro del campo del razonamiento formalizado consiste en la formalización de la metalógica de distintos sistemas lógicos. En esta línea se inscribe el artículo Formalization of propositional linear temporal logic in the Mizar system.

Su autor es Mariusz Giero (University of Bialystok).

Su resumen es

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.