Article View: comp.lang.prolog
Article #3923Re: Prolog and Modal Logic
From: Bob Tausworthe
Date: Sun, 26 Feb 1989 02:53
Date: Sun, 26 Feb 1989 02:53
12 lines
1010 bytes
1010 bytes
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
Technical Details
Message-ID:
<3720001@hpindda.HP.COM>Path:
arc1-ca.pugleaf.net!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!tozzReferences:
<4333@pt.cs.cmu.edu>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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