XML | TPTP |
<scl:formula xmlns:scl="http://scluripart"> <scl:quantifier scl:name="exists" scl:variable="x"> <scl:connective scl:name="implies"> <scl:predicate scl:name="p"> <scl:term scl:name="x"/> <scl:term scl:name="1"/> </scl:predicate> <scl:predicate scl:name="equal"> <scl:term scl:name="x"/> <scl:term scl:name="1"/> </scl:predicate> </scl:connective> </scl:quantifier> </scl:formula> | fof(the_name,axiom, ? [X] : ( p(X,1) => equal(X,1) ) ). |
Pros
| Pros
|
Cons
| Cons
|