Other
papers online
Theorem proving in modal logic using Boolean algebras
Greg
Mildenhall, Mark Reynolds
and Tim
Stokes.
Abstract
We use a uniform Boolean algebra rewrite rule approach to prove
tautologies in modal systems. including systems K, K4
(and hence also T and
S4) and K5. An algebraic expression derived from a compound proposition is
repeatedly rewritten and the proposition is a contradiction if and only if zero
is obtained; otherwise teh expression contains information about
counterexamples.
Full Paper
The latest
version will be online shortly.
Status
Submitted September 2002..
Online theorem-prover
This
theorem-prover uses the Boolean algebra idea to decide the satisfiability or
otherwise of formulas in various modal logics..
Bibtex
@misc{MRS:boolalg,
author="G. Mildenhall and M. Reynolds and
T. Stokes",
title="Theorem proving in modal logic using Boolean algebras",
year="submitted 2002",
}
References