diff --git a/README.md b/README.md
index 3b88127..bade9ee 100644
--- a/README.md
+++ b/README.md
@@ -39,7 +39,7 @@ A forward rule with `lingua:implication false` is an inference fuse.
 
 Lingua also supports reasoning with backward rules described in RDF as
 ```
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     RDF triples
diff --git a/VERSION b/VERSION
index af0b7dd..238d6e8 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-1.0.6
+1.0.7
diff --git a/lingua/ackermann.trig b/lingua/ackermann.trig
index f055bbc..7267ea0 100644
--- a/lingua/ackermann.trig
+++ b/lingua/ackermann.trig
@@ -27,7 +27,7 @@
 @prefix : <#>.
 
 # ackermann(x, y)
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     (var:X var:Y) :ackermann var:A.
@@ -41,7 +41,7 @@ _:ng2 {
 
 # ackermann(x, y, z)
 # succ (x=0)
-_:ng3 lingua:if _:ng4.
+_:ng3 lingua:hornb _:ng4.
 
 _:ng3 {
     (0 var:Y var:Z) :ackermann var:A.
@@ -53,7 +53,7 @@ _:ng4 {
 }
 
 # sum (x=1)
-_:ng5 lingua:if _:ng6.
+_:ng5 lingua:hornb _:ng6.
 
 _:ng5 {
     (1 var:Y var:Z) :ackermann var:A.
@@ -65,7 +65,7 @@ _:ng6 {
 }
 
 # product (x=2)
-_:ng7 lingua:if _:ng8.
+_:ng7 lingua:hornb _:ng8.
 
 _:ng7 {
     (2 var:Y var:Z) :ackermann var:A.
@@ -77,7 +77,7 @@ _:ng8 {
 }
 
 # exponentiation (x=3), tetration (x=4), pentation (x=5), hexation (x=6), etc
-_:ng9 lingua:if _:ng10.
+_:ng9 lingua:hornb _:ng10.
 
 _:ng9 {
     (var:X 0 var:Z) :ackermann 1.
@@ -87,7 +87,7 @@ _:ng10 {
     _:ng13 log:callWithCut true.
 }
 
-_:ng11 lingua:if _:ng12.
+_:ng11 lingua:hornb _:ng12.
 
 _:ng11 {
     (var:X var:Y var:Z) :ackermann var:A.
diff --git a/lingua/acp.trig b/lingua/acp.trig
index 8e0c7d9..6bd3205 100644
--- a/lingua/acp.trig
+++ b/lingua/acp.trig
@@ -16,7 +16,7 @@
     :anyOf :C;
     :noneOf :D.
 
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     var:Pol :pass :allOfTest.
@@ -36,7 +36,7 @@ _:ng4 {
     var:Test :has var:Field.
 }
 
-_:ng5 lingua:if _:ng6.
+_:ng5 lingua:hornb _:ng6.
 
 _:ng5 {
     var:Pol :pass :anyOfTest.
@@ -55,7 +55,7 @@ _:ng7 {
     var:Test :has var:Field.
 }
 
-_:ng8 lingua:if _:ng9.
+_:ng8 lingua:hornb _:ng9.
 
 _:ng8 {
     var:Pol :pass :noneOfTest.
diff --git a/lingua/backward.trig b/lingua/backward.trig
index d7706fb..ae7e7ef 100644
--- a/lingua/backward.trig
+++ b/lingua/backward.trig
@@ -10,7 +10,7 @@
 @prefix : <#>.
 
 # something is more interesting if it is greater
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     ("this" var:X) :moreInterestingThan ("that" var:Y).
diff --git a/lingua/complex.trig b/lingua/complex.trig
index f598910..426c213 100644
--- a/lingua/complex.trig
+++ b/lingua/complex.trig
@@ -11,7 +11,7 @@
 @prefix : <#>.
 
 # exponentiation
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     ((var:A var:B) (var:C var:D)) complex:exponentiation (var:E var:F).
@@ -34,7 +34,7 @@ _:ng2 {
 }
 
 # asin
-_:ng3 lingua:if _:ng4.
+_:ng3 lingua:hornb _:ng4.
 
 _:ng3 {
     (var:A var:B) complex:asin (var:C var:D).
@@ -63,7 +63,7 @@ _:ng4 {
 }
 
 # acos
-_:ng5 lingua:if _:ng6.
+_:ng5 lingua:hornb _:ng6.
 
 _:ng5 {
     (var:A var:B) complex:acos (var:C var:D).
@@ -93,7 +93,7 @@ _:ng6 {
 }
 
 # polar
-_:ng7 lingua:if _:ng8.
+_:ng7 lingua:hornb _:ng8.
 
 _:ng7 {
     (var:X var:Y) complex:polar(var:R var:Tp).
@@ -111,7 +111,7 @@ _:ng8 {
 }
 
 # dial
-_:ng9 lingua:if _:ng10.
+_:ng9 lingua:hornb _:ng10.
 
 _:ng9 {
     (var:X var:Y var:T) complex:dial var:Tp.
@@ -123,7 +123,7 @@ _:ng10 {
     (0 var:T) math:sum var:Tp.
 }
 
-_:ng11 lingua:if _:ng12.
+_:ng11 lingua:hornb _:ng12.
 
 _:ng11 {
     (var:X var:Y var:T) complex:dial var:Tp.
@@ -135,7 +135,7 @@ _:ng12 {
     (3.141592653589793 var:T) math:difference var:Tp.
 }
 
-_:ng13 lingua:if _:ng14.
+_:ng13 lingua:hornb _:ng14.
 
 _:ng13 {
     (var:X var:Y var:T) complex:dial var:Tp.
@@ -147,7 +147,7 @@ _:ng14 {
     (3.141592653589793 var:T) math:sum var:Tp.
 }
 
-_:ng15 lingua:if _:ng16.
+_:ng15 lingua:hornb _:ng16.
 
 _:ng15 {
     (var:X var:Y var:T) complex:dial var:Tp.
diff --git a/lingua/easter.trig b/lingua/easter.trig
index d06364e..d42143e 100644
--- a/lingua/easter.trig
+++ b/lingua/easter.trig
@@ -11,7 +11,7 @@
 @prefix : <#>.
 
 # calculate easter day
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     (var:x0) :easter (var:x34 var:x32).
diff --git a/lingua/edt.trig b/lingua/edt.trig
index fedcf22..1bb6e39 100644
--- a/lingua/edt.trig
+++ b/lingua/edt.trig
@@ -23,7 +23,7 @@ _:ng1 {
     <> log:imports <../../eye/reasoning/edt/test-dl.ttl>.
 }
 
-_:ng2 lingua:if _:ng3.
+_:ng2 lingua:hornb _:ng3.
 
 _:ng2 {
     var:X a var:D.
diff --git a/lingua/fibonacci.trig b/lingua/fibonacci.trig
index 01fdb53..ce4dcbb 100644
--- a/lingua/fibonacci.trig
+++ b/lingua/fibonacci.trig
@@ -10,7 +10,7 @@
 @prefix : <#>.
 
 # backward rules
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     (var:X) :fibonacci var:Y.
@@ -20,19 +20,19 @@ _:ng2 {
     (var:X 0 1) :fib var:Y.
 }
 
-_:ng3 lingua:if true.
+_:ng3 lingua:hornb true.
 
 _:ng3 {
     (0 var:A var:B) :fib var:A.
 }
 
-_:ng4 lingua:if true.
+_:ng4 lingua:hornb true.
 
 _:ng4 {
     (1 var:A var:B) :fib var:B.
 }
 
-_:ng5 lingua:if _:ng6.
+_:ng5 lingua:hornb _:ng6.
 
 _:ng5 {
     (var:X var:A var:B) :fib var:Y.
diff --git a/lingua/gps.trig b/lingua/gps.trig
index bc1291a..62a89b4 100644
--- a/lingua/gps.trig
+++ b/lingua/gps.trig
@@ -28,7 +28,7 @@
 @prefix : <#>.
 
 # find paths in the state space from initial state to goal state within limits
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     () gps:findpath (var:Goal var:Path var:Duration var:Cost var:Belief var:Comfort
@@ -40,7 +40,7 @@ _:ng2 {
         (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort 1)).
 }
 
-_:ng3 lingua:if _:ng4.
+_:ng3 lingua:hornb _:ng4.
 
 _:ng3 {
     () gps:findpath (var:Goal var:Path var:Duration var:Cost var:Belief var:Comfort
@@ -52,7 +52,7 @@ _:ng4 {
         (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort var:MaxStagecount)).
 }
 
-_:ng5 lingua:if _:ng6.
+_:ng5 lingua:hornb _:ng6.
 
 _:ng5 {
     () gps:findpaths (var:Maps var:Goal var:Path var:Duration var:Cost var:Belief var:Comfort var:Path var:Duration var:Cost var:Belief var:Comfort
@@ -63,7 +63,7 @@ _:ng6 {
     var:Goal log:call true.
 }
 
-_:ng7 lingua:if _:ng8.
+_:ng7 lingua:hornb _:ng8.
 
 _:ng7 {
     () gps:findpaths (var:Maps_s var:Goal var:Path_s var:Duration_s var:Cost_s var:Belief_s var:Comfort_s var:Path var:Duration var:Cost var:Belief var:Comfort
@@ -98,13 +98,13 @@ _:ng10 {
 }
 
 # counting the number of stages (a stage is a sequence of gps in the same map)
-_:ng11 lingua:if true.
+_:ng11 lingua:hornb true.
 
 _:ng11 {
     () gps:stagecount 1.
 }
 
-_:ng12 lingua:if _:ng13.
+_:ng12 lingua:hornb _:ng13.
 
 _:ng12 {
     var:A gps:stagecount var:B.
@@ -118,7 +118,7 @@ _:ng13 {
     (var:G 1) math:sum var:B.
 }
 
-_:ng14 lingua:if _:ng15.
+_:ng14 lingua:hornb _:ng15.
 
 _:ng14 {
     var:A gps:stagecount var:B.
@@ -133,7 +133,7 @@ _:ng15 {
 :i1 :location :Gent.
 
 # map of Belgium
-_:ng16 lingua:if _:ng17.
+_:ng16 lingua:hornb _:ng17.
 
 _:ng16 {
     :map-BE gps:description (_:ng18 true _:ng19 :drive_gent_brugge 1500.0 0.006 0.96 0.99).
@@ -151,7 +151,7 @@ _:ng19 {
     var:S :location :Brugge.
 }
 
-_:ng20 lingua:if _:ng21.
+_:ng20 lingua:hornb _:ng21.
 
 _:ng20 {
     :map-BE gps:description (_:ng22 true _:ng23 :drive_gent_kortrijk 1600.0 0.007 0.96 0.99).
@@ -169,7 +169,7 @@ _:ng23 {
     var:S :location :Kortrijk.
 }
 
-_:ng24 lingua:if _:ng25.
+_:ng24 lingua:hornb _:ng25.
 
 _:ng24 {
     :map-BE gps:description (_:ng26 true _:ng27 :drive_kortrijk_brugge 1600.0 0.007 0.96 0.99).
@@ -187,7 +187,7 @@ _:ng27 {
     var:S :location :Brugge.
 }
 
-_:ng28 lingua:if _:ng29.
+_:ng28 lingua:hornb _:ng29.
 
 _:ng28 {
     :map-BE gps:description (_:ng30 true _:ng31 :drive_brugge_oostende 900.0 0.004 0.98 1.0).
diff --git a/lingua/mi.trig b/lingua/mi.trig
index 8d2601c..f089f7a 100644
--- a/lingua/mi.trig
+++ b/lingua/mi.trig
@@ -10,13 +10,13 @@
 @prefix : <#>.
 
 # meta-interpreter rules
-_:mi_rule1_head lingua:if true.
+_:mi_rule1_head lingua:hornb true.
 
 _:mi_rule1_head {
     () :mi ().
 }
 
-_:mi_rule2_head lingua:if _:mi_rule2_body.
+_:mi_rule2_head lingua:hornb _:mi_rule2_body.
 
 _:mi_rule2_head {
     () :mi var:A.
@@ -29,7 +29,7 @@ _:mi_rule2_body {
 }
 
 # general head-body rules
-_:hb_rule1_head lingua:if true.
+_:hb_rule1_head lingua:hornb true.
 
 _:hb_rule1_head {
     () :headBody (_:hb_rule1_head_graph1 var:Rs var:Rs).
@@ -39,7 +39,7 @@ _:hb_rule1_head_graph1 {
     () :mi ().
 }
 
-_:hb_rule2_head lingua:if _:hb_rule2_body.
+_:hb_rule2_head lingua:hornb _:hb_rule2_body.
 
 _:hb_rule2_head {
     () :headBody (_:hb_rule2_head_graph1 var:B var:Rs).
@@ -63,7 +63,7 @@ _:hb_rule2_body_graph2 {
     () :mi var:Goals.
 }
 
-_:hb_rule3_head lingua:if _:hb_rule3_body.
+_:hb_rule3_head lingua:hornb _:hb_rule3_body.
 
 _:hb_rule3_head {
     () :headBody (_:hb_rule3_head_graph1 var:Rs var:Rs).
@@ -78,7 +78,7 @@ _:hb_rule3_body {
 }
 
 # natnum head-body rules
-_:natnum_hb_rule1_head lingua:if true.
+_:natnum_hb_rule1_head lingua:hornb true.
 
 _:natnum_hb_rule1_head {
     () :headBody (_:natnum_hb_rule1_head_graph1 var:Rs var:Rs).
@@ -88,7 +88,7 @@ _:natnum_hb_rule1_head_graph1 {
     () :natnum (0).
 }
 
-_:natnum_hb_rule2_head lingua:if _:natnum_hb_rule2_body.
+_:natnum_hb_rule2_head lingua:hornb _:natnum_hb_rule2_body.
 
 _:natnum_hb_rule2_head {
     () :headBody (_:natnum_hb_rule2_head_graph1 var:A var:Rs).
diff --git a/lingua/peano.trig b/lingua/peano.trig
index af49c14..47cd456 100644
--- a/lingua/peano.trig
+++ b/lingua/peano.trig
@@ -10,13 +10,13 @@
 @prefix : <#>.
 
 # add
-_:ng1 lingua:if true.
+_:ng1 lingua:hornb true.
 
 _:ng1 {
     (var:A 0) :add var:A.
 }
 
-_:ng2 lingua:if _:ng3.
+_:ng2 lingua:hornb _:ng3.
 
 _:ng2 {
     (var:A (:s var:B)) :add (:s var:C).
@@ -27,13 +27,13 @@ _:ng3 {
 }
 
 # multiply
-_:ng4 lingua:if true.
+_:ng4 lingua:hornb true.
 
 _:ng4 {
     (var:A 0) :multiply 0.
 }
 
-_:ng5 lingua:if _:ng6.
+_:ng5 lingua:hornb _:ng6.
 
 _:ng5 {
     (var:A (:s var:B)) :multiply var:C.
@@ -45,7 +45,7 @@ _:ng6 {
 }
 
 # factorial
-_:ng7 lingua:if _:ng8.
+_:ng7 lingua:hornb _:ng8.
 
 _:ng7 {
     var:A :factorial var:B.
@@ -55,13 +55,13 @@ _:ng8 {
     (var:A (:s 0)) :fac var:B.
 }
 
-_:ng9 lingua:if true.
+_:ng9 lingua:hornb true.
 
 _:ng9 {
     (0 var:A) :fac var:A.
 }
 
-_:ng10 lingua:if _:ng11.
+_:ng10 lingua:hornb _:ng11.
 
 _:ng10 {
     ((:s var:A) var:B) :fac var:C.
diff --git a/lingua/pi.trig b/lingua/pi.trig
index fff38af..bbbd25b 100644
--- a/lingua/pi.trig
+++ b/lingua/pi.trig
@@ -9,7 +9,7 @@
 @prefix var: <http://www.w3.org/2000/10/swap/var#>.
 @prefix : <#>.
 
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     (var:N var:Pi) :pi true.
@@ -21,13 +21,13 @@ _:ng2 {
     (3 var:A) math:sum var:Pi.
 }
 
-_:ng3 lingua:if true.
+_:ng3 lingua:hornb true.
 
 _:ng3 {
     (var:N var:N var:P var:P var:S) :pi true.
 }
 
-_:ng4 lingua:if _:ng5.
+_:ng4 lingua:hornb _:ng5.
 
 _:ng4 {
     (var:K var:N var:P0 var:P var:S) :pi true.
diff --git a/lingua/turing.trig b/lingua/turing.trig
index 511e18e..769c2bb 100644
--- a/lingua/turing.trig
+++ b/lingua/turing.trig
@@ -11,7 +11,7 @@
 @prefix : <#>.
 
 # interpreter for Turing machine
-_:ng1 lingua:if _:ng2.
+_:ng1 lingua:hornb _:ng2.
 
 _:ng1 {
     () :compute var:OutTape.
@@ -22,7 +22,7 @@ _:ng2 {
     (var:I () "#" ()) :find var:OutTape.
 }
 
-_:ng3 lingua:if _:ng4.
+_:ng3 lingua:hornb _:ng4.
 
 _:ng3 {
     var:List :compute var:OutTape.
@@ -34,7 +34,7 @@ _:ng4 {
     (var:I () var:Head var:Tail) :find var:OutTape.
 }
 
-_:ng5 lingua:if _:ng6.
+_:ng5 lingua:hornb _:ng6.
 
 _:ng5 {
     (var:State var:Left var:Cell var:Right) :find var:OutTape.
@@ -46,7 +46,7 @@ _:ng6 {
     (var:Next var:A var:B var:C) :continue var:OutTape.
 }
 
-_:ng7 lingua:if _:ng8.
+_:ng7 lingua:hornb _:ng8.
 
 _:ng7 {
     (:halt var:Left var:Cell var:Right) :continue var:OutTape.
@@ -58,7 +58,7 @@ _:ng8 {
     (var:R var:List) list:append var:OutTape.
 }
 
-_:ng9 lingua:if _:ng10.
+_:ng9 lingua:hornb _:ng10.
 
 _:ng9 {
     (var:State var:Left var:Cell var:Right) :continue var:OutTape.
@@ -68,7 +68,7 @@ _:ng10 {
     (var:State var:Left var:Cell var:Right) :find var:OutTape.
 }
 
-_:ng11 lingua:if _:ng12.
+_:ng11 lingua:hornb _:ng12.
 
 _:ng11 {
     (:left () var:Cell var:Right () "#" var:L) :move true.
@@ -78,7 +78,7 @@ _:ng12 {
     var:L list:firstRest (var:Cell var:Right).
 }
 
-_:ng13 lingua:if _:ng14.
+_:ng13 lingua:hornb _:ng14.
 
 _:ng13 {
     (:left var:List var:Cell var:Right var:Tail var:Head var:L) :move true.
@@ -89,13 +89,13 @@ _:ng14 {
     var:L list:firstRest (var:Cell var:Right).
 }
 
-_:ng15 lingua:if true.
+_:ng15 lingua:hornb true.
 
 _:ng15 {
     (:stop var:Left var:Cell var:Right var:Left var:Cell var:Right) :move true.
 }
 
-_:ng16 lingua:if _:ng17.
+_:ng16 lingua:hornb _:ng17.
 
 _:ng16 {
     (:right var:Left var:Cell () var:L "#" ()) :move true.
@@ -105,7 +105,7 @@ _:ng17 {
     var:L list:firstRest (var:Cell var:Left).
 }
 
-_:ng18 lingua:if _:ng19.
+_:ng18 lingua:hornb _:ng19.
 
 _:ng18 {
     (:right var:Left var:Cell var:List var:L var:Head var:Tail) :move true.
@@ -116,13 +116,13 @@ _:ng19 {
     var:L list:firstRest (var:Cell var:Left).
 }
 
-_:ng20 lingua:if true.
+_:ng20 lingua:hornb true.
 
 _:ng20 {
     () :reverse ().
 }
 
-_:ng21 lingua:if _:ng22.
+_:ng21 lingua:hornb _:ng22.
 
 _:ng21 {
     var:List :reverse var:Reverse.
diff --git a/lingua/universal.trig b/lingua/universal.trig
index 9511795..cf50523 100644
--- a/lingua/universal.trig
+++ b/lingua/universal.trig
@@ -9,14 +9,14 @@
 @prefix : <#>.
 
 # \Every x: type(x, Resource
-_:ng1 lingua:if true.
+_:ng1 lingua:hornb true.
 
 _:ng1 {
     var:X a rdfs:Resource.
 }
 
 # Everybody loves somebody who is lonely
-_:ng2 lingua:if _:ng3.
+_:ng2 lingua:hornb _:ng3.
 
 _:ng2 {
     var:A :loves var:B.
@@ -26,7 +26,7 @@ _:ng3 {
     (var:A) log:skolem var:B.
 }
 
-_:ng4 lingua:if _:ng5.
+_:ng4 lingua:hornb _:ng5.
 
 _:ng4 {
     var:B :is :lonely.
diff --git a/see.pl b/see.pl
index c07ad73..16db626 100644
--- a/see.pl
+++ b/see.pl
@@ -19,7 +19,7 @@
 :- use_module(library(semweb/turtle)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('SEE v1.0.6 (2024-03-23)').
+version_info('SEE v1.0.7 (2024-03-24)').
 
 help_info('Usage: see <options>* <data>*
 
@@ -72,7 +72,7 @@
 :- dynamic('<http://www.w3.org/1999/02/22-rdf-syntax-ns#rest>'/2).
 :- dynamic('<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'/2).
 :- dynamic('<http://www.w3.org/2000/01/rdf-schema#subClassOf>'/2).
-:- dynamic('<http://www.w3.org/2000/10/swap/lingua#if>'/2).
+:- dynamic('<http://www.w3.org/2000/10/swap/lingua#hornb>'/2).
 :- dynamic('<http://www.w3.org/2000/10/swap/lingua#implication>'/2).
 :- dynamic('<http://www.w3.org/2000/10/swap/lingua#nand>'/2).
 :- dynamic('<http://www.w3.org/2000/10/swap/lingua#query>'/2).
@@ -228,7 +228,7 @@
             ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I))),
     % create backward rules
     assertz(implies((
-            '<http://www.w3.org/2000/10/swap/lingua#if>'(B, A),
+            '<http://www.w3.org/2000/10/swap/lingua#hornb>'(B, A),
             findvars([A, B], V, alpha),
             list_to_set(V, U),
             makevars([A, B, U], [Q, I, X], beta(U)),
@@ -413,7 +413,7 @@
             conj_list(S, Y),
             append(Vl, X, U),
             makevars([M, S], [Q, I], alpha(U))
-            ), '<http://www.w3.org/2000/10/swap/lingua#if>'(Q, I))),
+            ), '<http://www.w3.org/2000/10/swap/lingua#hornb>'(Q, I))),
     % blow inference fuse
     assertz(implies((
             '<http://www.w3.org/2000/10/swap/lingua#nand>'(V, G),
diff --git a/see.pvm b/see.pvm
index ee6ce4c..e81ffed 100755
Binary files a/see.pvm and b/see.pvm differ