packages feed

HTab-1.5.4: examples/sat_no_mod/all1.frm

% Input file in the format of hylolib 1.3

signature
{

propositions { tall, strong, pretty, naive }
nominals     { alice, bob, jean, marie, unknown }
relations    { love,
               lovedBy : {inverseof love},
               canManipulate : {trclosureof lovedBy},
               know : {reflexive},
               touches : {symmetric},
               U : {universal},
               fatherOf,
               motherOf,
               parentOf : {equals {fatherOf,motherOf}},
               childOf : {inverseof parentOf},
               youngerThan : {transitive, subsetof childOf}
             }

}

theory {
 [U]((tall & strong) --> pretty);

 alice: ( strong  & !tall & !naive);
 bob: ( tall & !strong ) ;

 (alice:bob) v jean:<love>marie;

 bob:[lovedBy]naive;

 alice:<youngerThan>marie;
 marie:<youngerThan>bob;
 bob:<youngerThan>jean;

 unknown:<parentOf>alice

}

query (satisfiable? , "out1") {
 alice:<canManipulate>jean
}

query (satisfiable? , "out2") {
 unknown:<parentOf>jean
}

query (retrieve , "retrieve1") {
 <youngerThan>jean
}