<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="a"/>
</scl:predicate>
<scl:predicate scl:name="equal">
<scl:term scl:name="a"/>
<scl:term scl:name="X"/>
</scl:predicate>
</scl:connective>
</scl:quantifier>
</scl:formula>
| (set-logic UF)
(declare-sort sort1 0)
(declare-fun a ( ) sort1)
(declare-fun p ( sort1 sort1 ) Bool)
(assert
(exists ((?X sort1))
(=> (p ?X a)
(p a ?X))))
| fof(the_name,axiom,
? [X] :
( p(X,1)
=> equal(X,1) ) ).
|
Pros
- Free parser with every language
- Parsers build you a data structure
- Extensible, without affecting tools
| Pros
- Machine readable, writable (LISP)
- Focussed, but extensible
- Low storage overhead
| Pros
- Human and machine readable, writable (Prolog)
- Focussed, but extensible
- Medium storage overhead
- Identifiers (for proofs)
- Formula roles (to help ATPs)
|