Skip to content
Snippets Groups Projects
Commit d2313575 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Add resolution

parent ddb26294
No related branches found
No related tags found
No related merge requests found
Pipeline #20167 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 13 additions and 3 deletions
althelf/alethe.smt3
+ 13
− 3
View file @ d2313575
......@@ -25,9 +25,19 @@
:match-conclusion CL
)
% TODO
(declare-rule th_resolution)
(declare-rule resolution)
% TODO: sidecodition
(declare-rule th_resolution ((Cs Bool))
:premise-list Cs and
:requires ((check_resolution Cs CL) true)
:match-conclusion CL
)
% TODO: sidecodition
(declare-rule resolution ((Cs Bool))
:premise-list Cs and
:requires ((check_resolution Cs CL) true)
:match-conclusion CL
)
% TODO: sidecondition
(declare-rule tautology ((CL1 Bool))
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment