TPTP format for Skolemization steps

[Geoff Sutcliffe]

Hi all,

Thanks to intelligent input from varuious people, and in the context of the forthcoming ProoVer competition, it has been decided to simplify the way Skolemization steps are recorded in TPTP format derivations. The old skolemize() and bind() records are now combined into just one skolemize() record, ala ...

inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(Bride,sK0(Marriage))],[marriage])

( The old format separated that skolemize() record, ala ...

inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(Bride),bind(Bride,sK0(Marriage))],[marriage])

)

I believe this will be easy to change the output from ATP systems.

Cheers,

Geoff