Skolemization format update

[i-am-a-teapot]

Update for TPTP proof output for Skolemization for #843

[i-am-a-teapot]

The TSTP standard has changed to allow multiple skolemizations now, which this new format should be compatible with.
I ran some test files which looked fine, however there may be edge cases which I am not aware of (seems like skolemization works slighlty differently for higher order things)

[MichaelRawson]

Hi @i-am-a-teapot - thanks for the patch! Got some questions about it but it's looking good, we should have this in for CASC. :)

[MichaelRawson]

Good idea. I feel like this could be promoted to Signature.hpp if it doesn't exist already?

[MichaelRawson]

The first bool is whether the Skolem is for sorts or terms, I think. So: could this be a pair <unsigned, Term *> where the lhs is the variable being eliminated and the rhs is the Skolem term?

[i-am-a-teapot]

I modified it to use what you suggested and I think, it should be equivalent to check the term kind (if it is sort or not). (I also checked what is happening in Term and that seems to be ok, but maybe I am missing something)

In some tests I ran this seems to work, let me know if you see a problem with it!

[easychair]

Did I get it right that we drop a step from the proof (output)? If we have Skolemization, we should have a rule for it. It is essential for proof-checking. Or is it something else? Andrei

…

On Sat, 9 May 2026 at 08:33, Michael Rawson ***@***.***> wrote: ***@***.**** commented on this pull request. Hi @i-am-a-teapot <https://github.com/i-am-a-teapot> - thanks for the patch! Got some questions about it but it's looking good, we should have this in for CASC. :) ------------------------------ In Shell/Skolem.cpp <#849 (comment)>: > @@ -487,11 +493,11 @@ Formula* Skolem::skolemise (Formula* f) if (arity > 0) { def = new QuantifiedFormula(FORALL, vArgs.list(), def); } - - Unit* defUnit = new FormulaUnit(def,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::SKOLEM_SYMBOL_INTRODUCTION)); - UnitList::push(defUnit,_skolimizingDefinitions); + + //Unit* defUnit = new FormulaUnit(def,NonspecificInference0(UnitInputType::AXIOM,InferenceRule::SKOLEM_SYMBOL_INTRODUCTION)); + //UnitList::push(defUnit,_skolimizingDefinitions); I think this was the last use of SKOLEM_SYMBOL_INTRODUCTION. Maybe it can be removed now? ------------------------------ In Kernel/InferenceStore.cpp <#849 (comment)>: > @@ -82,6 +88,15 @@ void InferenceStore::recordIntroducedSymbol(Unit* u, SymbolType st, unsigned num pStack->push(SymbolId(st,number)); } +void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr<std::vector<unsigned>> inScopeVars) Why unique_ptr<vector<unsigned>> rather than just vector<unsigned>? ------------------------------ In Kernel/InferenceStore.cpp <#849 (comment)>: > @@ -82,6 +88,15 @@ void InferenceStore::recordIntroducedSymbol(Unit* u, SymbolType st, unsigned num pStack->push(SymbolId(st,number)); } +void InferenceStore::recordIntroducedSkolemSymbol(Unit* u, SymbolType st, unsigned number, unsigned replacedVar, std::unique_ptr<std::vector<unsigned>> inScopeVars) +{ + SymbolStack* pStack; + _introducedSymbols.getValuePtr(u->number(),pStack); + _introducedSymbolReplacedVars.insert(number, replacedVar); All of these fields are keyed by an unsigned and global to Vampire, right? What prevents us from Skolemnising X0 in different formulas and clashing here? ------------------------------ In Kernel/InferenceStore.cpp <#849 (comment)>: > @@ -555,19 +570,24 @@ struct InferenceStore::TPTPProofPrinter std::string getNewSymbols(std::string origin, std::string symStr) { return "new_symbols(" + origin + ",[" +symStr + "])"; } + + std::string getSymbolName(SymbolId sym) { + if (sym.first == SymbolType::FUNC ) { + return env.signature->functionName(sym.second); + } else if (sym.first == SymbolType::PRED){ + return env.signature->predicateName(sym.second); + } else { + return env.signature->typeConName(sym.second); + } + } Good idea. I feel like this could be promoted to Signature.hpp if it doesn't exist already? ------------------------------ In Shell/Skolem.hpp <#849 (comment)>: > @@ -103,7 +103,9 @@ class Skolem DHMap<unsigned,TermList> _varSorts; // for some heuristic evaluations after we are done - Stack<std::pair<bool, unsigned>> _introducedSkolemSyms; + + // Type, numberOfSymbol, Variable that was replaced by the skolem symbol, Variables that are in scope for a skolem symbol (for proof recording purposes) + Stack<std::tuple<bool, unsigned, unsigned, std::unique_ptr<std::vector<unsigned>>>> _introducedSkolemSyms; The first bool is whether the Skolem is for sorts or terms, I think. So: could this be a pair <unsigned, Term *> where the lhs is the variable being eliminated and the rhs is the Skolem term? — Reply to this email directly, view it on GitHub <#849 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BML7JC6V2M46J7Q27L4Z3NMRAVCNFSM6AAAAACYKXF7TWVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHM2DENJXGE3TSOBZHA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[i-am-a-teapot]

Skolemization previously consisted of two steps in our proof output: Introducing the symbol and another step which is the eliminating the existential.
The TSTP format is now slightly changed so we need to be more detailed for skolemization (so we keep recording skolemization!). Pretty much the simplest way of adhering to the required format, is to just do everything in one single step (printing all relevant detail in this single step) instead of splitting it in two.

[i-am-a-teapot]

In case you are wondering what is happening here:
I tried out a problem (see below), and (default) vampire crashed in tptp proof output mode due to not replacing the skolemized type in the polymorphic container(A), leaving an unbound variable. This should fix it I hope.

tff(container_type, type, (
    container: $tType > $tType
)).
tff(contains_pred, type, (
    contains: !> [A: $tType] : ( A * container(A) ) > $o
)).
tff(trigger_axiom, axiom, (
    ! [A: $tType] : 
      ! [X: A] : 
        ? [C: container(A)] : contains(A, X, C)
)).

% 4. Conjecture to complete valid TPTP problem state
tff(dummy_conjecture, conjecture, (
    ! [A: $tType] : 
      ! [X: A] : 
        ? [C: container(A)] : contains(A, X, C)
)).