Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!ucbvax!agate!helios.ee.lbl.gov!ncis.llnl.gov!lll-winken!uunet!lupine!infopiz!athertn!hpda!hpcuhb!hpindda!tozz
From: tozz@hpindda.HP.COM (Bob Tausworthe)
Newsgroups: comp.lang.prolog
Subject: Re: Prolog and Modal Logic
Message-ID: <3720001@hpindda.HP.COM>
Date: 26 Feb 89 02:53:34 GMT
References: <4333@pt.cs.cmu.edu>
Organization: HP Information Networks, Cupertino, CA
Lines: 12

I wrote a modal logic theorem prover which used tableau theorem
proving and unification for the binding. Worked pretty good except
the search space gets verry large very fast. The problem is that
you have to keep track of several "worlds". So rather than just
one search space with backtracking, I had to maintain multiple
search spaces with backtracking - uglee!!

It might be better if you customized the tableau rules for horn clauses,
this wuld be much more condusive to prolog language.

			Bob Tausworthe
			tozz@hpindda.hp.com