Other papers online

Theorem proving in modal logic using Boolean rings

Mark Reynolds and Tim Stokes

Abstract

We use Boolean rings and rewrite rules to prove theorems in the modal logic systems K and S5. The method is analogous to the use of disjunctive normal forms in Boolean algebra for proving or disproving classical tautologies, although a key difference is that a Boolean ring formalism is used.


Full Paper

Postscript draft version June 2001


Status

Submitted June 2001.


Online theorem-prover

This theorem-prover uses the Boolean Ring idea to decide the satisfiability or otherwise of formulas in the modal logics K or S5.


Bibtex

@misc{RS:boolring,
author="M. Reynolds and T. Stokes",
title="Theorem proving in modal logic using Boolean Rings",
year="in preparation 2000",
}


References