1 % Heinrich Heine Universitaet Duesseldorf
2 % (c) 2025-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 % Implementation of a Sequent Prover
6 % where we can use the ProB animator to perform proof steps
7 % proof rules taken/adapted from https://wiki.event-b.org/index.php/Inference_Rules
8 % rewrite rules taken/adapted from https://wiki.event-b.org/index.php/All_Rewrite_Rules
9 % the term representation is the one from ProB's well_definedness prover
10
11 :- module(sequent_auto_prover,[id_find_proof/5, bounded_find_proof/5]).
12
13 :- use_module(probsrc(module_information),[module_info/2]).
14 :- module_info(group,sequent_prover).
15 :- module_info(description,'This module provides automatic proof search algorithms').
16
17 % ---------------------
18
19 % auto-prover
20
21 :- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2, stop_ms_timer_with_debug_msg/2]).
22 :- use_module(library(between),[between/3]).
23
24 % iterative deepening search to find shortest proof:
25 id_find_proof(Sequent,Info,MaxDepth,Opts,Proof) :-
26 start_ms_timer(Timer),
27 between(1,MaxDepth,Depth),
28 if(find_proof(Sequent,Info,env(start_proof,Opts),Depth,Proof),
29 stop_ms_timer_with_debug_msg(Timer,found_proof(Proof)),
30 (stop_ms_timer_with_debug_msg(Timer,no_proof_found_until_depth(Depth)),fail)).
31
32 % do a single bounded search for a proof; may not find shortest proof
33 bounded_find_proof(Sequent,Info,MaxDepth,Opts,Proof) :-
34 start_ms_timer(Timer),
35 %set_prolog_flag(profiling,on),
36 if(find_proof(Sequent,Info,env(start_proof,Opts),MaxDepth,Proof),
37 stop_ms_timer_with_debug_msg(Timer,found_proof(Proof)),
38 (stop_ms_timer_with_msg(Timer,no_proof_found_until_depth(MaxDepth)), %print_profile,
39 fail)).
40
41 %:- block max_length(-,?).
42 %max_length([],_).
43 %max_length([_|T],Len) :- (Len=1 -> T=[] ; Len>1, L1 is Len-1, max_length(T,L1)).
44
45 find_proof(success(_),_Info,_,_,[]).
46 find_proof(Sequent,Info,Env,RemainingSteps,[Rule|TailProof]) :- RemainingSteps>0,
47 (find_auto_eager_rule(Rule,Sequent,Info,Env,NewSequent,NewInfo)
48 -> %tools_printing:indentws(RemainingSteps),write(eager(RemainingSteps,Rule,Env)),nl,
49 find_proof(NewSequent,NewInfo,Env,RemainingSteps,TailProof) % Commit to that step
50 ; %tools_printing:indentws(RemainingSteps),write(no_eager(RemainingSteps)),nl,
51 find_proof_no_eager(Sequent,Info,Env,RemainingSteps,[Rule|TailProof])
52 ).
53
54
55 find_proof_no_eager(Sequent,Info,env(LastRule,Opts),RemainingSteps,[Rule|TailProof]) :-
56 R1 is RemainingSteps-1,
57 (R1 < 1 -> NewSequent = success(_) % avoid trying out unnecessary rules at last step
58 ; true),
59 (member(disregard_rule(RX),Opts) -> dif(Rule,RX) ; true), % TODO: allow more rules to be disregarded
60 auto_trans_rule(Rule,Sequent,Info,LastRule,NewSequent,NewInfo),
61 (commit_to_rule(Rule) -> !, R2=RemainingSteps ; R2=R1),
62 find_proof(NewSequent,NewInfo,env(Rule,Opts),R2,TailProof).
63
64 % commit to this rule if it is possible; e.g., because it is an axiom
65 % as an alternative; we could move those rules to the eager rules (and then no try them again in the no_simp rules)
66 commit_to_rule(derive_goal). % if not disregarded, this provides a proof
67 commit_to_rule(cntr).
68 commit_to_rule(hyp).
69 commit_to_rule(hyp_or).
70 commit_to_rule(false_hyp).
71 commit_to_rule(true_goal).
72 commit_to_rule(eql).
73
74
75
76 % TODO: complete and select rules one wishes to apply in auto-mode
77 % default should only use selected hyps and not deselect or reselect hypotheses
78 % based on LastRule we can enforce a certain order (i.e., partial order reduction on rules)
79 % maybe we should disallow derive_goal
80 auto_trans_rule(Rule,Sequent,Info,_,NewSequent,Info) :-
81 sequent_prover:trans_with_info(Rule,Sequent,NewSequent,Info).
82 auto_trans_rule(Rule,Sequent,Info,_,NewSequent,Info) :-
83 sequent_prover:trans_desc_with_info(Rule,Sequent,NewSequent,Info,_).
84 auto_trans_rule(Rule,Sequent,Info,_,NewSequent,Info) :-
85 sequent_prover:trans_with_args(Rule,Sequent,NewSequent).
86 auto_trans_rule(Rule,Sequent,Info,LastRule,NewSequent,NewInfo) :-
87 LastRule = start_proof, % allow one reselect_hyp or induct_nat at the beginning
88 % TODO: restrict reselect_hyp to have a shared variabled?
89 sequent_prover:trans_with_args_info(Rule,state(Sequent,Info),state(NewSequent,NewInfo)).
90
91 :- use_module(probsrc(tools_strings), [atom_prefix/2]).
92 % rules which we will always fire and which we will not backtrack
93 find_auto_eager_rule(Rule,Sequent,Info,env(LastRule,Opts),NewSequent,Info) :-
94 member(use_eager_simplification,Opts),!,
95 % TODO: do not call create_descr
96 auto_eager_rule(Rule,Sequent,Info,LastRule,NewSequent).
97
98 % definition of those rules that we want to eagerly execute without backtracking
99 auto_eager_rule(Rule,Sequent,_Info,LastRule,NewSequent) :-
100 eager_rule(Rule,LastRule),
101 sequent_prover:trans_wo_info(Rule,Sequent,NewSequent).
102 auto_eager_rule(Rule,Sequent,_Info,_LastRule,NewSequent) :-
103 member(Rule,[and_l(_)]),
104 sequent_prover:trans_with_args(Rule,Sequent,NewSequent).
105 auto_eager_rule(Rule,Sequent,Info,_,NewSequent) :-
106 Rule = simplify_goal(_),
107 sequent_prover:trans_desc_simplification_rule(Rule,Sequent,NewSequent,Info,_Descr),
108 is_simplification_rule(Rule). % TODO: separate DERIV from SIMP rules; rules like DERIV_IMP can be applied infinitely often
109 %eager_rule(cntr,_).
110 %eager_rule(hyp,_).
111 %eager_rule(hyp_or,_).
112 eager_rule(false_hyp,_).
113 eager_rule(true_goal,_).
114 eager_rule(eql,_).
115 eager_rule(and_r,Last) :- % and_r can lead to longer proofs in case contradiction in Hyps
116 Last \= start_proof. % will split into two sub-proofs and we can re-add hyp only once
117 eager_rule(imp_r,_).
118 eager_rule(or_r,_).
119 % TODO: define more rules as eager; also axiom rules as eager; in particular if Cont is not success
120
121
122 is_simplification_rule(simplify_goal(Rule)) :- functor(Rule,F,_),atom_prefix('SIMP_',F).
123 is_simplification_rule(simplify_hyp(Rule)) :- functor(Rule,F,_),atom_prefix('SIMP_',F).