A Duplication and Loop Checking Free System for S4

Governatori, Guido (1996). A Duplication and Loop Checking Free System for S4. In: Miglioli, P., Moscato, U., Mundici, D. and Ornaghi, M. 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (Short Papers), Terrassini, Italy, (19-32). .

Document type: Conference Paper
Sub-type: Fully Published Paper
Collection: School of Information Technology and Electrical Engineering Publications
Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
s4.pdf s4.pdf application/pdf 151.49KB 363

Author Governatori, Guido
Title of paper A Duplication and Loop Checking Free System for S4
Conference Paper Type Fully Published Paper
Conference name 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (Short Papers)
Conference location Terrassini, Italy
Editor Miglioli, P.
Moscato, U.
Mundici, D.
Ornaghi, M.
Publication date 1996-01-01
Start page 19
End page 32
Abstract/Summary Most of the sequent/tableau based proof systems for the modal logic S4 need to duplicate formulas and thus are required to adopt some method of loop checking. In what follows we present a tableau-like proof system for S4, based on D'Agostino and Mondadori's classical KE, which is free of duplication and loop checking. The key feature of this system (let us call it KES4) consists in its use of (i) a label formalism which models the semantics of the modal operators according to the usual conditions for S4; and (ii) a label unification scheme which tells us when two labels "denote" the same world in the S4-model(s) generated in the course of proof search. Moreover, it uses special closure conditions to check models for putative contradictions.
Subjects 230101 Mathematical Logic, Set Theory, Lattices And Combinatorics
280403 Logics and Meanings of Programs
440106 Logic
Keyword modal logic
automated theorem provering
labelled tableaux
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status Unknown
 
Versions
Version Filter Type
Access Statistics: 183 Abstract Views, 363 File Downloads  -  Detailed Statistics
Created: Tue, 22 Mar 2005, 10:00:00 EST by Guido Governatori  -  Detailed History