--- a/NEWS Wed Mar 01 08:00:51 2023 +0100
+++ b/NEWS Wed Mar 01 08:00:51 2023 +0100
@@ -241,8 +241,7 @@
* Sledgehammer:
- Added an inconsistency check mode to find likely unprovable
conjectures. It is enabled by default in addition to the usual
- proving mode and can be controlled using the 'check_inconsistent'
- option.
+ proving mode and can be controlled using the 'falsify' option.
- Added an abduction mode to find likely missing hypotheses to
conjectures. It currently works only with the E prover. It is
enabled by default and can be controlled using the 'abduce'
--- a/src/Doc/Sledgehammer/document/root.tex Wed Mar 01 08:00:51 2023 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Mar 01 08:00:51 2023 +0100
@@ -100,7 +100,7 @@
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
and satisfiability-modulo-theories (SMT) solvers on the current goal, mostly
-to find proofs but also to find inconsistencies.%
+to find proofs but also to refute the goal.%
\footnote{The distinction between ATPs and SMT solvers is mostly
historical but convenient.}
%
@@ -276,8 +276,8 @@
\prew
\slshape
-vampire found an inconsistency\ldots \\
-vampire: The goal is inconsistent with these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
+vampire found a falsification\ldots \\
+vampire: The goal is falsified by these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
\postw
Sometimes Sledgehammer will helpfully suggest a missing assumption:
@@ -818,11 +818,11 @@
\opnodefault{prover}{string}
Alias for \textit{provers}.
-\opsmartx{check\_inconsistent}{dont\_check\_inconsistent}
-Specifies whether Sledgehammer should look for inconsistencies or for proofs. By
-default, it looks for both proofs and inconsistencies.
+\opsmartx{falsify}{dont\_falsify}
+Specifies whether Sledgehammer should look for falsifications or for proofs. By
+default, it looks for both.
-An inconsistency indicates that the goal, taken as an axiom, would be
+A falsification indicates that the goal, taken as an axiom, would be
inconsistent with some specific background facts if it were added as a lemma,
indicating a likely issue with the goal. Sometimes the inconsistency involves
only the background theory; this might happen, for example, if a flawed axiom is
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Mar 01 08:00:51 2023 +0100
@@ -159,20 +159,18 @@
fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
(problem as {state, subgoal, factss, ...} : prover_problem)
- (slice as ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), _)) name =
+ (slice as ((slice_size, abduce, falsify, num_facts, fact_filter), _)) name =
let
val ctxt = Proof.context_of state
val _ = spying spy (fn () => (state, subgoal, name,
- "Launched" ^ (if abduce then " (abduce)" else "") ^
- (if check_inconsistent then " (check_inconsistent)" else "")))
+ "Launched" ^ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "")))
val _ =
if verbose then
writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^
- (if abduce then " (abduce)" else "") ^
- (if check_inconsistent then " (check_inconsistent)" else "") ^ "...")
+ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "") ^ "...")
else
()
@@ -182,8 +180,7 @@
|> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
- |> prefix ("Facts in " ^ name ^ " " ^
- (if check_inconsistent then "inconsistency" else "proof") ^ ": ")
+ |> prefix ("Facts in " ^ name ^ " " ^ (if falsify then "falsification" else "proof") ^ ": ")
|> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -211,7 +208,7 @@
|> AList.group (op =)
|> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
in
- "Success: Found " ^ (if check_inconsistent then "inconsistency" else "proof") ^ " with " ^
+ "Success: Found " ^ (if falsify then "falsification" else "proof") ^ " with " ^
string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^
(if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
end
@@ -262,7 +259,7 @@
(if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then
(case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of
[] => "The goal is inconsistent"
- | facts => "The goal is inconsistent with these facts: " ^ commas facts)
+ | facts => "The goal is falsified by these facts: " ^ commas facts)
else
"The following facts are inconsistent: " ^
commas (map fst used_facts)))
@@ -292,8 +289,7 @@
fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode
has_already_found_something found_something writeln_result learn
- (problem as {state, subgoal, ...}) (slice as ((_, _, check_inconsistent, _, _), _))
- prover_name =
+ (problem as {state, subgoal, ...}) (slice as ((_, _, falsify, _, _), _)) prover_name =
let
val ctxt = Proof.context_of state
val hard_timeout = Time.scale 5.0 timeout
@@ -321,11 +317,11 @@
found_something = found_something "an inconsistency"}
end
- val problem as {goal, ...} = problem |> check_inconsistent ? flip_problem
+ val problem as {goal, ...} = problem |> falsify ? flip_problem
fun really_go () =
launch_prover params mode learn problem slice prover_name
- |> (if check_inconsistent then analyze_prover_result_for_inconsistency else
+ |> (if falsify then analyze_prover_result_for_inconsistency else
preplay_prover_result params state goal subgoal)
fun go () =
@@ -392,15 +388,15 @@
end
fun prover_slices_of_schedule ctxt goal subgoal factss
- ({abduce, check_inconsistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
+ ({abduce, falsify, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
...} : params)
schedule =
let
fun triplicate_slices original =
let
val shift =
- map (apfst (fn (slice_size, abduce, check_inconsistent, num_facts, fact_filter) =>
- (slice_size, abduce, check_inconsistent, num_facts,
+ map (apfst (fn (slice_size, abduce, falsify, num_facts, fact_filter) =>
+ (slice_size, abduce, falsify, num_facts,
if fact_filter = mashN then mepoN
else if fact_filter = mepoN then meshN
else mashN)))
@@ -418,7 +414,7 @@
| adjust_extra (extra as SMT_Slice _) = extra
fun adjust_slice max_slice_size
- ((slice_size0, abduce0, check_inconsistent0, num_facts0, fact_filter0), extra) =
+ ((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) =
let
val slice_size = Int.min (max_slice_size, slice_size0)
val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False})
@@ -426,15 +422,15 @@
(case abduce of
NONE => abduce0 andalso goal_not_False
| SOME max_candidates => max_candidates > 0)
- val check_inconsistent =
- (case check_inconsistent of
- NONE => check_inconsistent0 andalso goal_not_False
- | SOME check_inconsistent => check_inconsistent)
+ val falsify =
+ (case falsify of
+ NONE => falsify0 andalso goal_not_False
+ | SOME falsify => falsify)
val fact_filter = fact_filter |> the_default fact_filter0
val max_facts = max_facts |> the_default num_facts0
val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
in
- ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), adjust_extra extra)
+ ((slice_size, abduce, falsify, num_facts, fact_filter), adjust_extra extra)
end
val provers = distinct (op =) schedule
@@ -463,9 +459,8 @@
|> distinct (op =)
end
-fun run_sledgehammer (params as {verbose, spy, provers, check_inconsistent, induction_rules,
- max_facts, max_proofs, slices, ...})
- mode writeln_result i (fact_override as {only, ...}) state =
+fun run_sledgehammer (params as {verbose, spy, provers, falsify, induction_rules, max_facts,
+ max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state =
if null provers then
error "No prover is set"
else
@@ -476,17 +471,17 @@
val _ = Proof.assert_backward state
val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
- val found_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0
+ val found_proofs_and_falsifications = Synchronized.var "found_proofs_and_falsifications" 0
fun has_already_found_something () =
if mode = Normal then
- Synchronized.value found_proofs_and_inconsistencies > 0
+ Synchronized.value found_proofs_and_falsifications > 0
else
false
fun found_something a_proof_or_inconsistency prover_name =
if mode = Normal then
- (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1);
+ (Synchronized.change found_proofs_and_falsifications (fn n => n + 1);
(the_default writeln writeln_result) (prover_name ^ " found " ^
a_proof_or_inconsistency ^ "..."))
else
@@ -571,7 +566,7 @@
else
(learn chained_thms;
Par_List.map (fn (prover, slice) =>
- if Synchronized.value found_proofs_and_inconsistencies < max_proofs then
+ if Synchronized.value found_proofs_and_falsifications < max_proofs then
launch problem slice prover
else
(SH_None, ""))
@@ -581,7 +576,7 @@
fun normal_failure () =
(the_default writeln writeln_result
- ("No " ^ (if check_inconsistent = SOME true then "inconsistency" else "proof") ^
+ ("No " ^ (if falsify = SOME true then "falsification" else "proof") ^
" found");
false)
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Mar 01 08:00:51 2023 +0100
@@ -67,7 +67,7 @@
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 100 (* FUDGE *)
-(* desired slice size, abduce, check_inconsistent, desired number of facts, fact filter *)
+(* desired slice size, abduce, falsify, desired number of facts, fact filter *)
type base_slice = int * bool * bool * int * string
(* problem file format, type encoding, lambda translation scheme, uncurried aliases?,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Mar 01 08:00:51 2023 +0100
@@ -54,7 +54,7 @@
("overlord", "false"),
("spy", "false"),
("abduce", "smart"),
- ("check_inconsistent", "smart"),
+ ("falsify", "smart"),
("type_enc", "smart"),
("strict", "false"),
("lam_trans", "smart"),
@@ -87,7 +87,7 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("dont_spy", "spy"),
- ("dont_check_inconsistent", "check_inconsistent"),
+ ("dont_falsify", "falsify"),
("non_strict", "strict"),
("no_uncurried_aliases", "uncurried_aliases"),
("dont_learn", "learn"),
@@ -235,9 +235,9 @@
val abduce =
if mode = Auto_Try then SOME 0
else lookup_option lookup_int "abduce"
- val check_inconsistent =
+ val falsify =
if mode = Auto_Try then SOME false
- else lookup_option lookup_bool "check_inconsistent"
+ else lookup_option lookup_bool "falsify"
val type_enc =
if mode = Auto_Try then
NONE
@@ -271,7 +271,7 @@
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
- abduce = abduce, check_inconsistent = check_inconsistent, type_enc = type_enc, strict = strict,
+ abduce = abduce, falsify = falsify, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn,
fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Mar 01 08:00:51 2023 +0100
@@ -30,7 +30,7 @@
spy : bool,
provers : string list,
abduce : int option,
- check_inconsistent : bool option,
+ falsify : bool option,
type_enc : string option,
strict : bool,
lam_trans : string option,
@@ -141,7 +141,7 @@
spy : bool,
provers : string list,
abduce : int option,
- check_inconsistent : bool option,
+ falsify : bool option,
type_enc : string option,
strict : bool,
lam_trans : string option,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Mar 01 08:00:51 2023 +0100
@@ -83,8 +83,8 @@
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
minimize, preplay_timeout, induction_rules, ...} : params)
- (slice as ((_, _, check_inconsistent, _, fact_filter), slice_extra)) silent
- (prover : prover) timeout i n state goal facts =
+ (slice as ((_, _, falsify, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n
+ state goal facts =
let
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
(if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
@@ -92,7 +92,7 @@
val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
val params =
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
- type_enc = type_enc, abduce = SOME 0, check_inconsistent = SOME false, strict = strict,
+ type_enc = type_enc, abduce = SOME 0, falsify = SOME false, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false,
fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts),
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
@@ -118,7 +118,7 @@
(case outcome of
SOME failure => string_of_atp_failure failure
| NONE =>
- "Found " ^ (if check_inconsistent then "inconsistency" else "proof") ^
+ "Found " ^ (if falsify then "falsification" else "proof") ^
(if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
" (" ^ string_of_time run_time ^ ")"));
result