adding proof steps for inference fuse

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v11.2.5 (2024-12-30) adding proof steps for inference fuse
 v11.2.4 (2024-12-30) adding proof step for query
 v11.2.3 (2024-12-29) improving output for --logic-program
 v11.2.2 (2024-12-28) using :+ instead of := for bottom-up reasoning

VERSION

@@ -1 +1 @@
-11.2.4
+11.2.5

eye.pl

@@ -22,7 +22,7 @@
 :- catch(use_module(library(process)), _, true).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v11.2.4 (2024-12-30)').
+version_info('EYE v11.2.5 (2024-12-30)').
 
 license_info('MIT License
 
@@ -5302,8 +5302,18 @@
         (   Conc = true     % 3/
         ->  astep2((answer(Prem), step(Rule, Prem, true)))
         ;   (   Conc = false
-            ->  format("% inference fuse, return code 2~n", []),
+            ->  astep2(step(Rule, Prem, false)),
+                format("% inference fuse, return code 2~n", []),
                 portray_clause(user_output, fuse(Prem), [indent(2)]),
+                (   step(_, _, _)
+                ->  format("~n% proof steps~n", []),
+                    (   step(R, P, C),
+                        portray_clause(user_output, step(R, P, C), [indent(2)]),
+                        fail
+                    ;   true
+                    )
+                ;   true
+                ),
                 throw(halt(2))
             ;   (   term_variables(Conc, [])
                 ->  Concl = Conc

logic-programming/output/fuse.pl

@@ -2,3 +2,8 @@
 
 % inference fuse, return code 2
   fuse(('<urn:example:color>'('<urn:example:stone>', '<urn:example:black>'), '<urn:example:color>'('<urn:example:stone>', '<urn:example:white>'))).
+
+% proof steps
+  step((false:+'<urn:example:color>'(A, '<urn:example:black>'), '<urn:example:color>'(A, '<urn:example:white>')),
+       ('<urn:example:color>'('<urn:example:stone>', '<urn:example:black>'), '<urn:example:color>'('<urn:example:stone>', '<urn:example:white>')),
+       false).

logic-programming/output/proof-by-contradiction.pl

@@ -2,3 +2,11 @@
 
 % inference fuse, return code 2
   fuse('<urn:example:Mortal>'('<urn:example:Socrates>')).
+
+% proof steps
+  step(('<urn:example:Mortal>'(A):+'<urn:example:Human>'(A)),
+       '<urn:example:Human>'('<urn:example:Socrates>'),
+       '<urn:example:Mortal>'('<urn:example:Socrates>')).
+  step((false:+'<urn:example:Mortal>'(_)),
+       '<urn:example:Mortal>'('<urn:example:Socrates>'),
+       false).