A Mechanized Proof Procedure for Free Intensional Logics

A MEX:EINIZED PKXJF PRX:EOORE FOR FREE mrENSICNAL lOGICS*

Raynond D. Gumb Terrple University Philadelphia, Permsylvania 19122

Included am:mgst the intensional logics are tmse dealing with obligation (deontic logic), necessity (nodal logic), tirre (tense logic), and various other intensional concepts. These logics were developed to fonnalize the serrantics of nat­ ural language discourses. The intensional logics studied here are extensions of sare of the senten­ ial logics known as the normal intensional logics. These logics include the nodal logics K, M, B, S4, arrl SS arrl their deontic arrl tense logic comterparts. The closure of the accessibility relation in these logics can be readily ccrtputed, a convenient property for mechanizing proofs.

In free logics, iixli vidual nanes need not have a referent, arrl the dcmain of discourse is not required to be non-arpty. There is general agreement that a quantified intensional logic must have a free quantificational base if it is to capture the logic of natural language discourses. By having a free base, it is possible, e.g., for t\\0 ~rlds to be c:arpatible where, in one ~rld, it is declared that sarething exists arrl, in the other ~rld, that nothing exists. Or a tenn can refer at one tirre rut not at another. M:>re tech­ nically, neither the Barcan formula ('t/x Ql\~ 0\lxA in a nodal logic) nor its converse (0 V xA=> lrJ x. Ql\) are provable in a free intensional logic.

If the free intensional logics are fO\.ll'rl to constitute the possible logical bases of sanantic descriptions of natural languages, as many be­ lieve, then an adequate systan for autanatic natural language processing must handle these logics correctly. A mechanized proof procedure for these logics must be devised for such tasks as disambiguating discourses, question-answering, arrl guiding rule-governed behavior.

Failure of the Barcan formula arrl its con­ verse rules out natural extensions of t\\0 theoren proving techniques in starrlard first-order logic to the free intensional logics. First, in the tradition of Gentzen, Beth, arrl Snullyan, the device of using a single tree in a derivation is difficult to develop, as the same tenn on the one arrl only tree might have to refer in one place rut not in another. Secorrl, the resolution rreth:xl presut:POseS a prenex normal fonn theoren, rut this fails in the free intensional logics. If a can­ p..ltational rrethod could be developed for the free intensional logics using either the device of a single tree or resolution, it is likely that it wa.lld be sanewhat counter-intuitive.

*This ~rk was supported in part by a Tarple University Sunner Research Fellowship.

Instead, a mechanized proof procedure is pre­ sented in which there is a tree for each "possible ~rld" arrl a scheme of branch numbering to identi­ fy corresporxling branches of different trees. This tree rreth:xl provides a new view of what con­ stitutes a proof, arrl an appropriate sanantics is developed. It awlies to an ordered set of sets of sentences (known as an evolving theory) arrl not just to a single set of sentences as other deductive systens do. Interleaved derivations are carried out in a finite number of ~rlds (trees) which interact. These interacting proofs could also be executed in parallel.