No way of instantiating a new KB

[javiermtorres]

Neither the ProverState data constructor nor the zeroKB are exported in the KnowledgeBase module. I don't see a way of instantiating a KB to carry out proofs on it. Would it be enough to export zeroKB in the module?

Thanks, and regards,

Javier Torres

[ddssff]

Hello! There are examples of the use of the KnowledgeBase module in Tests/Chiou0.hs, but I'm not certain that more exports wouldn't be necessary for other applications. I've just added a .ghci file that should allow you to do the following:

% ghci
λ :load Tests/Chiou0.hs
λ let conjecture = pApp "Kills" [fApp "Jack" [], fApp "Tuna" []] :: TFormula
λ pPrint conjecture
Kills(Curiosity,Tuna)
λ pPrint (runProver' Nothing (loadKB sentences >> theoremKB conjecture))
(False,
 [(() => (Kills(Curiosity,Tuna)), []),
  ((Animal(Tuna) AnimalLover(Curiosity)) => (), []),
  ((Animal(Tuna) Dog(y') Owns(Curiosity,y)) => (), []),
  ((Animal(Tuna) Owns(Curiosity,y)) => (), []),
  ((AnimalLover(Curiosity)) => (), []),
  ((AnimalLover(Curiosity) Cat(Tuna)) => (), []),
  ((Cat(Tuna) Dog(y') Owns(Curiosity,y)) => (), []),
  ((Cat(Tuna) Owns(Curiosity,y)) => (), []),
  ((Dog(y') Owns(Curiosity,y)) => (), []),
  ((Kills(Jack,Tuna)) => (), []), ((Owns(Curiosity,y)) => (), [])])

(Is this even the right answer?) There are quasi quoters in the atp-haskell package (module Data.Logic.ATP.Parser) that should make it easier to create inputs, but I'm not clear if there are ambiguities when you type something like

λ [fof|Kills(Jack,Tuna)|]
pApp (fromString "Kills")["Jack", "Tuna"]
λ pPrint [fof|Kills(Jack,Tuna)|]
Kills(Jack,Tuna)
λ ([fof|Kills(Jack,Tuna)|] :: TFormula) == (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []] :: TFormula)
False

Let me know what you discover, and if you have more questions/suggestions/requests.

[javiermtorres]

Thank you very much for the surprisingly fast response ^_^ I'm trying to build epistemic and temporal logics on top of these modules, and I'll probably need a finer control over the KB (if you're interested, to build a graph of KBs, possibly inheriting part of the contents, using some temporal operators, and maybe in a semi-declarative way, like e.g. "the set of all possible worlds for which p is True and q is True" ). But I'll take a look at the Chiou0 module, and come back to you. At least for the moment it should be possible for me to work using your code sample.

Thanks again, and regards,

Javier

[ddssff]

Sounds exciting! Do you have any good references where I could read about these logics?

[ddssff]

By the way, logic-classes is sort of a vestigial package. Its guts moved into atp-haskell. I'm not sure whether what is left has a coherent story. (And I haven't really looked at it for a while.)

[javiermtorres]

Give me a couple of days. I can give you some pretty theory-heavy papers but I don't fully understand those myself :D so I want to find an intro to modal logics and Kripke frames, and introduce temporal and epistemic modalities from there. A good description of the end goal is https://en.wikipedia.org/wiki/Induction_puzzles . A couple of people and myself are working on this project in the field of games and narratives.

[javiermtorres]

I mainly use atp-haskell (more or less, the code is heavily parameterized :-S and I'm no haskell master), but now that I need to manage sets of propositions and run proofs on them I'm turning to logic-classes. We thought about using natural deduction, but it seems overkill right now. The seereason package is exactly the size we need :)

[ddssff]

Great! There are errors in the test suite that should probably be investigated. To be honest, I didn't fully understand the mechanisms being used when I wrote/translated the code. I'm pretty clear about the stuff in atp-haskell now, but the logic-classes stuff is a little foggy.

[javiermtorres]

Hi,

It seems (at least in 1.7) that the theoremKB function handles ProverT', while loadKB uses StateT (ProverState (ImplicativeForm lit)) directly (type ProverT inf = StateT (ProverState inf)), but I guess it should not be a big deal.

However, it seems they both have a dependency towards the Atom class, as defined in the Data.Logic.Classes.Atom package:

class Atom atom term v | atom -> term v where
substitute :: Map.Map v term -> atom -> atom
allVariables :: atom -> Set.Set v
freeVariables :: atom -> Set.Set v
unify :: Map.Map v term -> atom -> atom -> Failing (Map.Map v term)
match :: Map.Map v term -> atom -> atom -> Failing (Map.Map v term)
-- ^ Very similar to unify, not quite sure if there is a difference
foldTerms :: (term -> r -> r) -> r -> atom -> r
isRename :: atom -> atom -> Bool
getSubst :: Map.Map v term -> atom -> Map.Map v term

Do you know if there is something similar in the atp-haskell package? The IsAtom class is much less detailed, and I can't locate similar functions in it (Maybe the Unif package???).

Thanks a lot, and regards,

Javier

[ddssff]

The IsAtom class is the successor to Atom. I guess there's a bit of work to do to finish off that transition. Hmm...

[javiermtorres]

I was expecting that :D My take is to try and reuse as much as possible from Unif and Resolution, probably leveraging on the relations between IsAtom, IsTerm and V in a similar way as it is done in Atom. I will post here possible replacements for the functions defined in the Atom class, based on ATP modules. Is that ok?

[ddssff]

That would be awesome. I'm looking at Harrison's book right now, and the set of support algorithm in Data.Logic.Resolution seems to correspond to the algorithm in Data.Logic.ATP.Prolog. So adapting that to what you are doing might be another way to go.

[javiermtorres]

Thanks a lot for checking that out ^_^ I'm going to sleep now, but I'll try to check Prolog then. I'll keep you updated here!

[javiermtorres]

Ok, Implicative was ported without modification. Could you confirm that Implicative would be OK in the ATP package?

[ddssff]

I'm not sure I understand what you mean.

[javiermtorres]

Ok, it's just that I need to read the book XD My question was along the
lines of, if we have Tableaux and Meson, can we build an analogue of
KnowledgeBase but resting on those theorem proving methods? Taking into
account that I don't know what algorithm KnowledgeBase currently uses (the
Prolog algos, according to your previous answers?).

So, instead of porting KB as it is, we may just mimic it by building a set
of sentences and checking the validity of new sentences with Tableaux and
Meson. But I need to read the book to check that I'm not just spewing BS :)

On Wed, Sep 28, 2016 at 12:52 AM, David Fox [email protected]
wrote:

I'm not sure I understand what you mean.

—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
#2 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/AEZSy3HVZJ_7Z5DxoGa3lDC73j-UiDKeks5quZ5LgaJpZM4J9kiP
.

[ddssff]

Yes, I have to believe that would be both correct and easy. Good news is that its near the beginning of the material on actual proof methods (that is, right after the coverage of propositional and first order logic and unification), and the algorithms are already ported in atp-haskell. The index has an entry for "set of support" which refers to page 200. So with any luck it should work out...

[ddssff]

https://github.com/daijo/fol

[javiermtorres]

Thanks a lot! Working on it! I'm reading KB more carefully now, so I should
be able to come up with something using already existing algorithms in
atp-haskell. It will be a good exercise for my Haskell ;)

On Wed, Sep 28, 2016 at 8:26 PM, David Fox [email protected] wrote:

https://github.com/daijo/fol

—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
#2 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/AEZSy-rVDN2o76PiVnv-bdDcSzFh524Pks5qurE4gaJpZM4J9kiP
.