let paramodulation = bool "paramodulation" params in
let full = bool "full" params in
let superposition = bool "superposition" params in
- let what = string "what" params in
- let other = string "other" params in
+ let target = string "target" params in
+ let table = string "table" params in
let subterms_only = bool "subterms_only" params in
- let demodulate = bool "demodulate" params in
+ let caso_strano = bool "caso_strano" params in
+ let demod_table = string "demod_table" params in
(* the real tactic *)
let auto_tac dbd (proof, goal) =
let normal_auto () =
debug_print (lazy "USO PARAMODULATION...");
(* try *)
try
- let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
+ let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full (proof, goal) in
prerr_endline (Saturation.get_stats ());
rc
with exn ->
match superposition with
| true ->
ProofEngineTypes.mk_tactic
- (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate)
+ (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table)
| _ -> ProofEngineTypes.mk_tactic (auto_tac dbd)
;;
[g1;g2] ->
let proof'',goals =
ProofEngineTypes.apply_tactic
- (auto_tac ~params:["paramodulation","on"] ~dbd) (proof'',g2)
+ (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2)
in
let proof'',goals =
ProofEngineTypes.apply_tactic
| CicUnification.UnificationFailure msg
| CicTypeChecker.TypeCheckerFailure msg ->
raise (ProofEngineTypes.Fail msg))
+
+let pp_proofterm = Equality.pp_proofterm;;