First-order modal tableaux (Q1104913)

We describe simple semantic tableau based theorem provers for four standard modal logics, in both propositional and first-order versions. These theorem provers are easy to implement in Prolog, have a behavior that is straightforward to understand, and provide natural places for the incorporation of heuristics. Background theory is presented, and implementations of one propositional and one first-order version are given.