Repository navigation
Input type cleanup 1 - #1051
Merged
Merged
Input type cleanup 1#1051
Conversation
…with the NEGATED_CONJETURE formula role
…eliminates the actual one
The mode has no known users and has fallen behind the rest of the prover: it never prints symbol declarations, so its output cannot be read back for typed input, and it runs a preprocessing prefix of its own, so what it selects can differ from what -ss axioms selects when proving. For instance, it drops the axiom in fof(ax,axiom,p(a) => $distinct(a,b)). fof(goal,conjecture,p(a) => a != b). because that axiom is triggered only by the $distinct marker literal, which normal preprocessing has already expanded by the time it runs SInE. The same functionality is available as --mode preprocess -ss axioms, since with the clausifier off Preprocess::preprocess stops right after SInE. It prints declarations, and handles higher-order input via the usual FOOL elimination. Compared to the old mode, it also normalises interpreted symbols and adds theory axioms; for typed input, add --theory_axioms off to keep the output readable, as preprocess prints clauses without sorts. Besides the mode, this removes Options::setSineSelection, which only the mode called. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
TPTPPrinter::printUnit negated any formula of input type CONJECTURE, so that the unit the parsers derive by CONJECTURE_NEGATION would print as the stated conjecture. The same applied to everything further down the derivation, and the code needed Formula::quantify, a cleanup guard and special cases for the polarity of the result. It also lost the conjecture's name, since the name belongs to the stated unit, which was never printed: fof(goal,conjecture,~p(b)). vampire --mode output prints tff(u3,conjecture, ~p(b)) vampire --mode preprocess prints tff(u3,conjecture, ~p(b)) Now units are printed as they are, and the role tells them apart: a unit of input type CONJECTURE is a conjecture only if it is the stated one, with rule INPUT; anything derived from it is a negated_conjecture. --mode output needs the stated conjecture, so it now prints the parent of a CONJECTURE_NEGATION unit, which also brings back its name: vampire --mode output prints tff(goal,conjecture, ~p(b)) vampire --mode preprocess prints tff(u3,negated_conjecture, (~ ~p(b))) A visible consequence is that preprocess and preprocess2 now print negated_conjecture, as tpreprocess already did. Their output is not official TPTP, and it re-reads as Unsatisfiable rather than Theorem, which is accepted. This also makes the "CONJECTURE as inputType is evil" block in preprocessMode redundant, so it is removed. Its reason went away with the parser's single conjecture restriction; tpreprocess still prints negated_conjecture, now through the role rule, because the unit is already negated. The ProofOutput tests are updated to match, dropping the cases for the removed negation branches and the test of its variable closure, which the TPTP parser asserts is not needed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
mezpusz
reviewed
Nov 6, 2026
| } else { | ||
| negateFormula = true; | ||
| } | ||
| if (unit->inputType() == UnitInputType::CONJECTURE && unit->inference().rule() != InferenceRule::INPUT) { |
Contributor
There was a problem hiding this comment.
Shouldn't we assert here that unit->inference().rule() == InferenceRule::CONJECTURE_NEGATION? Are there other cases too?
Collaborator
Author
There was a problem hiding this comment.
This actually propagates through the inferences of preprocessing and further. There is a unique start of this, the CONJECTURE_NEGATION, but it does not end and we still (probably) want to keep recalling a unit comes from the conjecture.
Contributor
There was a problem hiding this comment.
I think this is better, but actually throws up another question for me. Should we print role negated_conjecture for everything that is tainted by the conjecture in proof output? It seems that e.g. E does so and it actually occurs in the example that Geoff uses (https://tptp.org/UserDocs/QuickGuide/Derivations.html , Formula c_0_8).
On the other hand https://proover-competition.github.io/rules-format/ disagrees here.
So if at a later point this function is used, we have this "taint" while in proof printing we don't.
If we don't want to go with this taint, I am thinking that maybe we should just leave this decision to the caller of the function (and defaulting to plain)?
Collaborator
Author
There was a problem hiding this comment.
I wouldn't mind that (the "leave this decision to the caller of the function (and defaulting to plain)").
Your link also made me notice my new rule name is breaking "A negated conjecture step must: use the inference rule name negated_conjecture;". What do you think, should I roll back or convince the future organizers they are wrong?
Contributor
There was a problem hiding this comment.
I like the new name, it's in the present tense, like "binary resolution" - we don't say "binary resolved". Would be happy to lobby the organisers.
Contributor
There was a problem hiding this comment.
I am sure these rules are able to be bent :) So I would then say that we leave the decision to what the rule is to the caller and fix that problem in that way!
mezpusz
reviewed
Nov 6, 2026
MichaelRawson
approved these changes
Nov 7, 2026
Contributor
|
This is unrelated to the implementation.
I tried to argue with Geoff ages ago about the use of "conjecture" but
arguing with Geoff about logic is like discussing paintings with
color-blind.
The problem is that the proof now must contain formulas that are not
consequences of the negation of the goal (or introduced definitions). I
told him that the proof should only contain such formulas and roles should
be used as *annotations of where formulas come from*.
Thus, using the "negated conjecture" in the proof is correct, but the use
of "conjecture" is wrong. The consequence of Geoff's decision is that we
must have i*nferences deriving ~A from A* - this is already sufficient to
see that something is wrong. Early Vampires did not display the conjucture
in the proof - only the negated conjecture.
There are other justtifications of why Geoff's decision is wrong. E.g. CNF
cannot contain conjectures. Of what we call an "axiom" in CNF is not an
axiom - it is derived from an axiom - if we consider "axiom" as an
annotation "comes from an axiom", then everything becomes right. Another
question - can an input contain two conjectures? If yes, how should we
understand them? Note that a CNF can contain several negated conjectures -
total mess.
Andrei
…On Sun, 8 Nov 2026 at 10:07, Michael Rawson ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In Shell/TPTPPrinter.cpp
<#1051 (comment)>:
> const char* role = TPTPOutput::inputRole(unit->inputType());
- bool negateFormula = false;
- if (unit->inputType() == UnitInputType::CONJECTURE) {
- if (unit->isClause()) {
- role = TPTPOutput::Role::NEGATED_CONJECTURE;
- } else {
- negateFormula = true;
- }
+ if (unit->inputType() == UnitInputType::CONJECTURE && unit->inference().rule() != InferenceRule::INPUT) {
I like the new name, it's in the present tense, like "binary resolution" -
we don't say "binary resolved". Would be happy to lobby the organisers.
—
Reply to this email directly, view it on GitHub
<#1051?email_source=notifications&email_token=ABVY4BNXSG35QEQ3ZOROEBL5YBAVXA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKOBRG42DOMJYGE32M4TFMFZW63VKON2WE43DOJUWEZLEUVSXMZLOOSWGM33PORSXEX3DNRUWG2Y#discussion_r4505825814>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABVY4BKH66BWCSJSS72FF3L5YBAVXAVCNFSNUABEKJSXA33TNF2G64TZHMYTQMBWG44TCMB3JFZXG5LFHM3DENBVGMYTSNJSGSQXMAQ>
.
Triage notifications, keep track of coding agent tasks and review pull
requests on the go with GitHub Mobile for iOS
<https://github.com/notifications/mobile/ios/ABVY4BLGEY6SVK7SHTVONGL5YBAVXA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKOBRG42DOMJYGE32M4TFMFZW63VKON2WE43DOJUWEZLEUVSXMZLOOSVGM33PORSXEX3JN5ZQ>
and Android
<https://github.com/notifications/mobile/android/ABVY4BNPWQNSRLNAJYN3ET35YBAVXA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKOBRG42DOMJYGE32M4TFMFZW63VKON2WE43DOJUWEZLEUVSXMZLOOSXGM33PORSXEX3BNZSHE33JMQ>.
Download it today!
You are receiving this because you are subscribed to this thread.Message
ID: <vprover/vampire/pull/1051/review/5817471817 ***@***.***
.com>
|
i-am-a-teapot
approved these changes
Nov 9, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Making things more sensible our yesterday's discussion. Version 1.
UnitInputTypeandisClausestatus.axiom_selectionmode, which is better achieved asmode preprocessunder some non-default sine settingsInferenceRuleis calledCONJECTURE_NEGATIONto better distinguish it from theUnitInputTypetclausifyWhat's next? Two big things I will only prepare later:
UnitInputTypein the sense of general-purpose analogue of formulas' TPTP role (which only makes sense for the input formulas) from the Unit's conjecture-relatedness status (which propagates through inferences and is used by various heuristics)