Presentation of Classical Propositional Tableaux on Program Design Premises

Autor:	Michelini, Juan, Tasistro, Alvaro
Rok vydání:	2015
Předmět:	Computer Science - Computers and Society Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	We propose a presentation of classical propositional tableaux elaborated by application of methods that are noteworthy in program design, namely program derivation with separation of concerns. We start by deriving from a straightforward specification an algorithm given as a set of recursive equations for computing all models of a finite set of formulae. Thereafter we discuss the employment of data structures, mainly with regard to an easily traceable manual execution of the algorithm. This leads to the kinds of trees given usually as constituting the tableaux. The whole development strives at avoiding gaps, both of logical and motivational nature. Comment: Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, Jo\~ao Marcos, Mar\'ia Manzano, Sophie Pinchinat, Fran\c{c}ois Schwarzentruber
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1507.03676 Zobrazit plný text záznamu View this record from Arxiv