srd@PROOF.ERGO.CS.CMU.EDU (Scott Dietzen) (02/23/89)
I am interested in recent work on extending Prolog (or other logic programming paradigms) to modal logic. Any pointers would be appreciated. Thank you. Scott Dietzen (dietzen@cs.cmu.edu) -- Scott Dietzen Arpanet: srd@theory.cs.cmu.edu Uucp: ...!seismo!theory.cs.cmu.edu!srd --
tozz@hpindda.HP.COM (Bob Tausworthe) (02/26/89)
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