Synthesising Terminating Tableau Calculi for Relational Logics: Invited Paper

Schmidt, R. A. (2011)

In de Swart, H. (ed), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science, Vol. 6663, Springer, 40-49. BiBTeX, DOI Link.

Tableau-based deduction is an active and well-studied area of several branches of logic and automated reasoning. In this paper we discuss the challenge of automatically generating tableau calculi from the semantic specification of logics, while guaranteeing soundness, completeness and termination, when possible.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 11 Jun 11
Copyright © 2011 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk