Maude-help mailing list

[PATRICK BROWNE <patrick.browne AT dit.ie>]

Hi,

 I am trying to represent theories expressed in first order predicate logic as Maude theories.  I am not sure if this can be done!  Below is one of my efforts

 I use the BOOL module for predicates, Skolem functions for existential variables, and the deduction theorem for proof.

Any feedback on my efforts would be welcome.

Regards,

Pat

*** Example from http://www.indiana.edu/~gasser/Q351/rtp_example.html

***  Tuna is a cat

***  All cats are animals

***  Jack owns a dog.

***  Every dog owner is an animal lover.

***  No animal lover kills an animal.

***  Either Jack or Curiosity killed the cat, who is named Tuna.

***  Prove Curiosity killed the cat

fth CURIOSITY is

protecting BOOL .

sort Elt .

ops dog cat animal : Elt -> Bool .

op  animalLover : Elt -> Bool .

op owns : Elt Elt -> Bool .

op kill : Elt Elt -> Bool .

ops Jack Tuna Curiosity : -> Elt .

*** The function id is used to denote non-dependent existential variables

op id : Elt -> Elt . 

*** A Skolem function to denote  existential variables that depends on a universal

op sk : Elt -> Elt .

*** LHS of each equation includes information on wheather the variable is universal or existential (lazy).

op s1 : Elt  -> Bool  [strat (0)] .

op s2 : Elt Elt  -> Bool   [strat (1 0)] . 

op s3 : Elt Elt  -> Bool .

ops s4 s5 :  -> Bool .

op s6 : Elt  -> Bool .

vars x y : Elt .

eq s1(id(x))  = dog(x) and owns(Jack,x) .

eq s2(x,sk(y)) = dog(sk(y)) and owns(x,sk(y)) implies  animalLover(x) .

eq s3(x,y) = animalLover(x) implies (animal(y) implies not kill(x,y)) .

eq s4 = kill(Jack,Tuna) or kill(Curiosity,Tuna) .

eq s5 = cat(Tuna) .

eq s6(x) = cat(x) implies animal(x) .

endfth

fth PROOF is

including CURIOSITY .

*** Existential instantiation: Assumes that both existentials have the same value.

op aDog : -> Elt .

eq id(aDog) = aDog .

eq sk(Jack) = aDog .

endfth

*** Deduction theorem with Universal and Existential instantiation.

red (s1(id(aDog)) and s2(Jack,sk(Jack)) and s3(Jack,Tuna) and s4 and s5 and s6(Tuna)) implies kill(Curiosity,Tuna) .

This email originated from DIT. If you received this email in error, please delete it from your system. Please note that if you are not the named addressee, disclosing, copying, distributing or taking any action based on the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to Grangegorman