[isabelle] ON Isabelle/SMT counter_example

   . I have two questions on Isabelle/SMT.

1) is the intermedia formula which is tranformed from HOL formula, and
will be fed
 into z3.
2) is the counterexample format after z3 checked the formula has

I use the following as a running example.

 lemma "P --> Q" using [[smt_trace]] by smt;

by my understanding,

The intermediate formula should be a propostion logical formula in SMT
format for

The counter-ex should say an assignment: P: true; and

but I'm confued about the Isabelle's trace output. Can anyone explain,
(see Isabelle's output below):

Does the terms f1 f2 make sense?

The assignment only says P = ??.SMT.term_true, but this is not complete,
Q is False is also needed to specify?


  f1 = ??.SMT.term_true
    f2 = ??.SMT.term_false

The counterexample output is just as follows:
SMT: Assertions:
  \<not> (P \<longrightarrow> Q)

SMT: Names:
    S1 = bool
    f1 = ??.SMT.term_true
    f2 = ??.SMT.term_false
    f3 = P
    f4 = Q

SMT: Problem:
  (benchmark Isabelle
  :status unknown
  :logic AUFLIA
  :extrasorts ( S1)
  :extrafuns (
    (f1 S1)
    (f2 S1)
    (f3 S1)
    (f4 S1)
  :assumption (not (= f1 f2))
  :assumption (not (implies (= f3 f1) (= f4 f1)))
  :formula true)
  ; solver: z3
  ; timeout: 20.0
  ; random seed: 1
  ; arguments:
  ; -rs:1
  ; MODEL=true
  ; -smt

SMT: Invoking SMT solver "z3" ...

SMT: Solver:

SMT: Result:
  f2 -> S1!val!1
  f1 -> S1!val!0
  f3 -> S1!val!0
  f4 -> S1!val!2

SMT: Solver z3: Counterexample found (possibly spurious):
  P = ??.SMT.term_true

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.