Prove

Given a conjecture (an SMT-LIB2 assertion or a natural language claim), determine whether it holds universally. The method is standard: negate the conjecture and check satisfiability. If the negation is unsatisfiable, the original is valid. If satisfiable, the model is a counterexample.

Step 1: Prepare the negated formula

Action: Wrap the conjecture in (assert (not ...)) and append (check-sat)(get-model).

Expectation: A complete SMT-LIB2 formula that negates the original conjecture with all variables declared.

Result: If the negation is well-formed, proceed to Step 2. If the conjecture is natural language, run encode first.

Example: to prove that (> x 3) implies (> x 1):

(declare-const x Int)
(assert (not (=> (> x 3) (> x 1))))
(check-sat)
(get-model)

Step 2: Run the prover

Action: Invoke prove.py with the conjecture and variable declarations.

Expectation: The script prints valid, invalid (with counterexample), unknown, or timeout. A run entry is logged to z3agent.db.

Result: On valid: proceed to explain if the user needs a summary. On invalid: report the counterexample directly. On unknown/timeout: try simplify first, or increase the timeout.

python3 scripts/prove.py --conjecture "(=> (> x 3) (> x 1))" --vars "x:Int"

For file input where the file contains the full negated formula:

python3 scripts/prove.py --file negated.smt2

With debug tracing:

python3 scripts/prove.py --conjecture "(=> (> x 3) (> x 1))" --vars "x:Int" --debug

Step 3: Interpret the output

Action: Read the prover output to determine validity of the conjecture.

Expectation: One of valid, invalid (with counterexample), unknown, or timeout.

Result: On valid: the conjecture holds universally. On invalid: the model shows a concrete counterexample. On unknown/timeout: the conjecture may require auxiliary lemmas or induction.

Parameters

Either conjecture (with vars) or file must be provided.