Geoff's Party Points

Verification of Skolemization steps is a thorny issue
Possible approaches include ...
- Adding some weakened form of axiom of choice
- Using Hilbert ε-terms
- Using a trusted Skolemizer
Some steps in that direction ...
- Eliminating quantifiers one at a time
- Identifying the new Skolem symbol

The TSTP syntax has a way to record new symbols

In the BNF, an inference record, add useful info, for a new symbol, where the first argument is skolem, and the new symbol list contains the new Skolem symbol. Example

fof(pel47_14a,axiom,
    ! [X] :
      ( snail(X)
     => ? [Y] :
          ( plant(Y)
          & eats(X,Y) ) ) ).

fof(c_0_30,plain,
    ! [X24] :
      ( ( plant(esk3_1(X24))
        | ~ snail(X24) )
      & ( eats(X24,esk3_1(X24))
        | ~ snail(X24) ) ),
    inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa),new_symbols(skolem,[esk3_1])],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pel47_14a])])])])]) ).

For verification, it would be nicer to have the Skolemization step separate, and record which variable was Skolemized (assuming variables have been uniquely renamed). Example:

fof(pel47_14a,axiom,
    ! [X] :
      ( snail(X)
     => ? [Y] :
          ( plant(Y)
          & eats(X,Y) ) ) ).

fof(c_0_30_1,plain,
    ! [X24] :
      ( ~ snail(X24)
      | ? [Y] :
          ( plant(Y)
          & eats(X,Y) ) ),
    inference((variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pel47_14a])])) ).

fof(c_0_30_2,plain,
    ! [X24] :
      ( ~ snail(X24)
      | ( plant(esk3_1(X24))
        & eats(X,esk3_1(X24)) ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[esk3_1]),skolemized(Y)],[c_0_30_1]) ).

fof(c_0_30,plain,
    ! [X24] :
      ( ( plant(esk3_1(X24))
        | ~ snail(X24) )
      & ( eats(X24,esk3_1(X24))
        | ~ snail(X24) ) ),
    inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_30_2])]) ).

Producing an ε-term for the new Skolem symbol would be useful for LampdaPi. Example:

fof(c_0_30_1,plain,
    ! [X24] :
      ( ~ snail(X24)
      | ? [Y] :
          ( plant(Y)
          & eats(X,Y) ) ),
    inference((variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pel47_14a])])) ).

fof(c_0_30_2,plain,
    ! [X24] :
      ( ~ snail(X24)
      | ( plant(esk3_1(X24))
        & eats(X,esk3_1(X24)) ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[esk3_1])],[c_0_30_1]) ).

//----Using # for epsilon, per [GA01]
fof(c_0_30_2_epsilon,plain,
    ! [X24] :
      ( esk3_1(X24)
      = # [Y] : 
          ( plant(Y)
          & eats(X24,Y) ) ) ).

Geoff's Party Points

Persistent ATP Data

StarExec Containerization

Verified Proofs and Models in CASC

Recording Skolemization Steps

New TPTP Format for Interpretations

Advertisement: The TPTP World Tour