Message-ID:

It is the theory which decides what can be observed. -- Albert Einstein

mP FORMAL PROOF

<3c6c8b97-b24b-40ad-ac55-b7ef911d59ben@googlegroups.com>

https://www.novabbs.com/devel/article-flat.php?id=47190&group=comp.theory#47190

X-Received: by 2002:a05:6214:192a:b0:621:3d97:5da5 with SMTP id es10-20020a056214192a00b006213d975da5mr266868qvb.10.1683648246546;
Tue, 09 May 2023 09:04:06 -0700 (PDT)
X-Received: by 2002:a05:6830:1295:b0:6a4:47d5:5121 with SMTP id
z21-20020a056830129500b006a447d55121mr796621otp.2.1683648246189; Tue, 09 May
2023 09:04:06 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!1.us.feeder.erje.net!feeder.erje.net!border-1.nntp.ord.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Tue, 9 May 2023 09:04:06 -0700 (PDT)
Injection-Info: google-groups.googlegroups.com; posting-host=2001:8004:11a0:4a9c:1c9f:f7d:2cc4:7302;
posting-account=EsDGawkAAAAN6xcF2fi-X0yb3ECD-3_I
NNTP-Posting-Host: 2001:8004:11a0:4a9c:1c9f:f7d:2cc4:7302
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <3c6c8b97-b24b-40ad-ac55-b7ef911d59ben@googlegroups.com>
Subject: mP FORMAL PROOF
From: grahamco...@gmail.com (Graham Cooper)
Injection-Date: Tue, 09 May 2023 16:04:06 +0000
Content-Type: text/plain; charset="UTF-8"
Lines: 77

by: Graham Cooper - Tue, 9 May 2023 16:04 UTC

------ 1 0/0 -----
query :- tru [ ad [ s 0 ] [ s 0 ] ANS ]
------------
---------- BEGIN 1 ---------
tru [ ad [ s 0 ] [ s 0 ] ANS ]
1>>> R = [ ad [ s 0 ] [ s 0 ] ANS ]

------ 2 0/0 -----
tru R :- fact R
------------
---------- BEGIN 2 ---------
fact R
1> R = [ ad [ s 0 ] [ s 0 ] ANS ]
2>>> X = [ s 0 ]
NOT FOUND

****** 2 ******
R = [ ad [ s 0 ] [ s 0 ] ANS ] X = [ s 0 ]
****************

PROGRAM 2

------ 3 1/1 -----
tru R :- if L R tru L
------------
---------- BEGIN 3 ---------
if L R
2> R = [ ad [ s 0 ] [ s 0 ] ANS ]
3>> L = [ ad A [ s B ] C ]
3>>> A = 0
3>>> B = [ s 0 ]
3>> ANS = C
---------- BEGIN 4 ---------
tru L
3> L = [ ad A [ s B ] C ]
[ ad A [ s B ] C ]-->[ ad 0 [ s B ] C ]
4>>> R = [ ad 0 [ s B ] C ]

------ 5 0/0 -----
tru R :- fact R
------------
---------- BEGIN 5 ---------
fact R
4> R = [ ad 0 [ s B ] C ]
5>>> X = 0
NOT FOUND

****** 5 ******
R = [ ad 0 [ s B ] C ] X = 0
****************

PROGRAM 2

------ 6 1/1 -----
tru R :- if L R tru L
------------
---------- BEGIN 6 ---------
if L R
5> R = [ ad 0 [ s B ] C ]
6>> L = [ ad A [ s B ] C ]
NOT FOUND

****** 6 ******
R = [ ad 0 [ s B ] C ] L = [ ad A [ s B ] C ]
****************
NOT FOUND
BACKTRACK

6> L = [ ad A [ s B ] C ]
NOT FOUND

****** 3 ******
R = [ ad [ s 0 ] [ s 0 ] ANS ] L = [ ad A [ s B ] C ] A = 0 B = [ s 0 ] ANS = C
****************
NOT FOUND

It is the theory which decides what can be observed. -- Albert Einstein

devel / comp.theory / mP FORMAL PROOF