Maude-help mailing list

[Patrick Browne <patrick.browne AT dit.ie>]

Hi,
SEM[1] is a system for enumerating finite models of first-order
many-sorted theories. SEM performs model generation.  MACE[2] is perhaps
a better known model generator. In SEM all axioms are expressed in terms
of predicates, logical negation (-) and logical or (|) and equality. The
exact details of  SEM are not important to my questions.
The fact that SEM (and MACE) produce all models for a finite theory (or
specification) is the motivation for my questions. My hope is that
Maude's search command could also produce such a set of models.
If Maude can produce these models, then I can ask the more specific
question of how finite models of my specification (mainly the IN
predicate) could be produced using the Maude Search command.


In the attached file  there is a Maude approximation (MODELCHECK) of a
SEM example. I suppose that the SEM example could really be ignored and
I could simplify my questions as follows:
“Can  Maude enumerate all models of  the attached MODELCHECK specification?”
This question assumes that my SEM-to-Maude is OK.

Regards,
Pat



[1] Zhang, J. and Zhang, H. (1995). Sem: a system for enumerating models.
 http://dli.iiit.ac.in/ijcai/IJCAI-95-VOL%201/pdf/039.pdf


[2] MACE is bundled with PROVER9 (previously know as OTTER)
  http://www.cs.unm.edu/~mccune/mace4/



Brian Rice wrote:
> I was also curious but hoping it would be voluntarily explained.
> 
> On Tue, Oct 5, 2010 at 2:30 PM, Emmanuel Castro
> <emmanuel.castro AT laposte.net
>  
> <mailto:emmanuel.castro AT laposte.net>>
>  wrote:
> 
>     Sorry to show my ignorance, but what is SEM?
>     _______________________________________________
>     Maude-help mailing list
>     
> Maude-help AT cs.uiuc.edu
>  
> <mailto:Maude-help AT cs.uiuc.edu>
>     http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
> 
> 
> -- 
> -Brian T. Rice
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help


This message has been scanned for content and viruses by the DIT Information 
Services E-Mail Scanning Service, and is believed to be clean. 
http://www.dit.ie***  
*** SEM[1] like MACE [3] can generate models from specifications.
*** Given a set of axioms SEM can find their models.
*** I am trying to replicate some SEM specifications from [2] using Maude.
*** I am hoping to use the Maude search command will enumerate the models.
*** SEM produces all true and false cases from a model e.g.
*** in(Maine,Bangor) = $F
*** in(Maine,Maine) = $T
*** in(Maine,I95) = $F
*** in(Maine,river1) = $F
*** in(Orono,Maine) = $T
*** For the moment, I am interested in just the true cases.
*** Below is my attempt to encode the original SEM specification[2] in Maude.
*** I am focusing only on the IN predicate and some of its axioms.
*** The command search in(x,y) =>*  true does not produce any true results.
*** If the data equations are  reversed then the command search  true =>*  
in1(x,y) produces some true results.
*** My questions are:
***                 1) Can Maude approximate SEM model generation?
***                 2) If Maude can provide some SEM functionality, how can I 
make my code provide that functionality?
*** 
*** [1] Zhang, J. and Zhang, H. (1995). Sem: a system for enumerating models. 
*** http://dli.iiit.ac.in/ijcai/IJCAI-95-VOL%201/pdf/039.pdf
*** 
*** [2] Semantic Interoperability Of Geospatial Ontologies: A Model-Theoretic 
Analysis, James A. Farrugia, PhD thesis 2007
*** http://www.library.umaine.edu/theses/pdf/FarrugiaJA2007.pdf
*** 
*** [3] MACE is bundled with PROVER9 (previously know as OTTER)
***   http://www.cs.unm.edu/~mccune/mace4/

mod MODELCHECK is
sort Thing .
op Route2 : -> Thing .
op Orono : -> Thing .
op Bangor : -> Thing .
op Maine : -> Thing .
op I95 : -> Thing .
op river1 : -> Thing .
***  Functions
op state : Thing -> Bool .
op town : Thing -> Bool .
op road : Thing -> Bool .
op river : Thing -> Bool .
op in : Thing Thing -> Bool .
op through : Thing Thing -> Bool .


vars x y z : Thing .

*** IN is reflexive, antisymmetric, and transitive
eq   [IN1] : in(x,x) = true .
ceq  [IN2] : (x == y) = true if in(y,x)  and in(x,y) [nonexec]  .
ceq  [IN3] : in(x,z) = true if (in(x,y) and in(y,z)) [nonexec]  .  


*** towns, roads, rivers, and states are all pairwise disjoint
eq town(x) and road(x)   = false .
eq town(x) and  river(x)   = false .
eq town(x) and  state(x)   = false .
eq road(x) and  river(x)   = false .
eq road(x) and  state(x)   = false  .
eq river(x) and  state(x)   = false  .

*** if x and y are different roads/rivers/towns/states, then x can’t be IN y
*** don't think I need to check both in(x,y) and in(y,x)
ceq  in(x,y)   = false if road(x) and road(y) and  not(x == y) .
ceq  in(x,y)   = false if river(x) and river(y) and  not(x == y) .
ceq  in(x,y)   = false if town(x) and town(y) and  not(x == y) .
ceq  in(x,y)   = false if state(x) and state(y) and  not(x == y) .

*** if x is a state and y is a town,  then x is NOT IN y
ceq [townState] : in(x,y) = false if (state(x) and town(y))  .


*** data: does not seem to work when ..=> true
*** the command search, in1(x,y) =>*  true, gives not true results
*** rl town(Orono)  => true .
*** rl town(Bangor)  => true .
*** rl road(Route2)  => true .
*** rl road(I95)   => true .
*** rl state(Maine)  => true .
*** rl river(river1)  => true .
*** rl in(Orono, Maine)  => true .
*** rl in(Bangor, Maine)  => true .

*** data : I get some results when true => ..
rl true =>  town(Orono)   .
rl true =>  town(Bangor)  .
rl true =>  road(Route2)  .
rl true => road(I95) .
rl true =>  state(Maine)   .
rl true =>  river(river1)   .
rl true =>  in(Orono, Maine)  .

endm

eof

search  true =>*  in1(x,y) .
gives some results
 
 
%% Original SEM specification file ch5O2.in.
%% Sorts
( thing : Route2, Orono, Bangor, Maine, I95, river1 )
%% Functions
{ state : thing -> BOOL }
{ town : thing -> BOOL }
{ road : thing -> BOOL }
{ river : thing -> BOOL }
{ in : thing thing -> BOOL }
{ through : thing thing -> BOOL }
%% Clauses (Axioms)
% IN is reflexive, antisymmetric, and transitive
[ in(x,x) ]
[ x=y | -in(x,y) | -in(y,x) ]
[ -in(x,y) | -in(y,z) | in(x,z)]
% THROUGH is antisymmetric and transitive
[ x=y | -through(x,y) | -through(y,x) ]
[ -through(x,y) | -through(y,z) | through(x,z)]

% towns, roads, rivers, and states are
% all pairwise disjoint
[ -town(x) | -road(x) ]
[ -town(x) | -river(x) ]
[ -town(x) | -state(x) ]
[ -road(x) | -river(x) ]
[ -road(x) | -state(x) ]
[ -river(x) | -state(x) ]

% if x and y are different roads/rivers/towns/states,
% then x is NOT IN y
[ x=y | -road(x) | -road(y) | -in(x,y) ]
[ x=y | -road(x) | -road(y) | -in(y,x) ]
[ x=y | -river(x) | -river(y) | -in(x,y) ]
[ x=y | -river(x) | -river(y) | -in(y,x) ]
[ x=y | -town(x) | -town(y) | -in(x,y) ]
[ x=y | -town(x) | -town(y) | -in(y,x) ]
[ x=y | -state(x) | -state(y) | -in(x,y) ]
[ x=y | -state(x) | -state(y) | -in(y,x) ]

% if x is a town/state/river and y is a road,
% then x is NOT IN y
[ -town(x) | -road(y) | -in(x,y) ]
[ -state(x) | -road(y) | -in(x,y) ]
[ -river(x) | -road(y) | -in(x,y) ]

% if x is a road/town/state and y is a river,
% then x is NOT IN y
[ -road(x) | -river(y) | -in(x,y) ]
[ -town(x) | -river(y) | -in(x,y) ]
[ -state(x) | -river(y) | -in(x,y) ]

% if x is a state and y is a town,
% then x is NOT IN y
[ -state(x) | -town(y) | -in(x,y) ]

% if x is a state and y is a town,
% then x does NOT go THROUGH y
[ -state(x) | -town(y) | -through(x,y) ]

% if x is a town/state and y is a road,
% then x does NOT go THROUGH y
[ -town(x) | -road(y) | -through(x,y) ]
[ -state(x) | -road(y) | -through(x,y) ]

% if x is a town/state/road and y is a river,
% then x does NOT go THROUGH y
[ -town(x) | -river(y) | -through(x,y) ]
[ -state(x) | -river(y) | -through(x,y) ]
[ -road(x) | -river(y) | -through(x,y) ]

% if x is a town/state and y is a town,
% then x does NOT go THROUGH y
[ -town(x) | -town(y) | -through(x,y) ]
[ -state(x) | -town(y) | -through(x,y) ]
% if x goes THROUGH y, then y is NOT IN x
[ -through(x,y) | -in(y,x) ]


% data
[ town(Orono) ]
[ town(Bangor) ]
[ road(Route2) ]
[ road(I95) ]
[ state(Maine) ]
[ river(river1) ]
[ in(Orono, Maine) ]
[ in(Bangor, Maine) ]
[ through(river1, Bangor) ]
[ through(river1, Orono) ]
[ through(river1, Maine) ]
[ through(I95, Bangor) ]
[ through(I95, Orono) ]
[ through(I95, Maine) ]
[ through(Route2, Bangor) ]
[ through(Route2, Orono) ]
[ through(Route2, Maine) ]
[ -through(Orono, Maine) ]
[ -through(Bangor, Maine) ]
%  There are 1250 models of ch5O2.in.