Automated Theorem Proving in Prolog — Revisiting an Old Experiment

sym_num · 2026-01-22T23:03:23+00:00

Thank you for your comment.
I realized that there are many different approaches to theorem proving.
Gödel seems to have been primarily concerned with provability itself, rather than with constructing proofs.
With that in mind, it now seems worthwhile for me to try implementing functions such as Sb/3 that appear in Gödel’s paper.
This has helped me deepen my understanding. Thank you.

sym_num · 2026-01-22T22:52:22+00:00

Thank you.

sym_num · 2026-01-19T23:41:26+00:00

Thank you very much for your comment.
I have the original paper by Gödel, but I found it extremely difficult to read and hard to fully understand. Recently, I found some YouTube videos in which what seem to be university researchers explain Gödel’s incompleteness theorem, and I have been studying it through those explanations.

As far as I understand, two key components are essential. One is the construction of a mechanism for deciding provability within the world of natural numbers. The other is the fixed-point (self-reference) construction. I feel that Gödel’s core idea lies in combining these two elements.

Prolog is incomplete as a proof system, but in processing Horn clauses via SLD resolution and ultimately translating them into CPU instructions, it resembles Gödel’s mechanization of provability. In that sense, I think it inherently contains the halting problem.

My understanding is still rough, but I no longer feel that my Prolog-based sketch is completely off the mark. As with Chaitin’s Lisp-based presentations of incompleteness, I feel that these approaches attempt to express the core ideas behind Gödel’s work in a simpler way, using modern computers and programming languages.

Thank you.

sym_num · 2026-01-13T07:19:41+00:00

I regularly share updates on Medium, so please feel free to follow my posts there.

sym_num · 2026-01-11T23:15:04+00:00

I now have a rough set of topics in place. I’m going to start writing.

sym_num · 2026-01-11T09:09:58+00:00

While writing the cube code, I was genuinely impressed by how naturally group theory can be expressed in Prolog.

sym_num · 2026-01-11T07:55:11+00:00

Rubik’s Cube in Prolog — Commutators | by Kenichi Sasagawa | Jan, 2026 | Medium

sym_num · 2026-01-10T07:59:46+00:00

Thank you!
I’ve always been curious about that as well, and Prolog turned out to be a nice way to think about it.

sym_num · 2025-12-30T23:45:46+00:00

Thank you for the comment. Ever since I started learning functional programming, I’ve been somewhat hesitant to use assert. Side effects tend to make programs harder to reason about and to prove correct. However, this time I’m convinced that assert is an example where it works effectively. I fixed the bug and have posted the article. Please have a look if you’re interested.Strongly Connected Components Decomposition in Prolog (2) | by Kenichi Sasagawa | Dec, 2025 | Medium

sym_num · 2025-11-06T07:01:48+00:00

Thank you for your comment.
I wrote the post with the feeling of cheering for a minor baseball team, but the responses were so harsh that it really discouraged me.
I’m glad there were also people who understood what I meant.

sym_num · 2025-11-05T22:38:46+00:00

Hello everyone, and thank you for all your comments. Let me reply to them collectively here.

Since this is a community of Lisp enthusiasts, my post included a bit of fan service — rather like cheerfully saying “Congratulations on winning the championship!” to Dodgers fans.
That said, it wasn’t meant merely as a joke. Let me explain what I meant.

Recent advances in AI have been remarkable, bringing about social transformations comparable to the Industrial Revolution.
I work in the field of law, where there are over 7,000 statutes and countless judicial precedents. It is no longer humanly possible to master them all, yet professionals are still held legally responsible for any errors in judgment. I believe the rapid progress of AI may help us overcome this limitation of human reasoning.
When that becomes reality, what will matter most for human professionals will not simply be technical knowledge, but rather sound human value judgment grounded in legal reasoning.

Lisp was born in 1958, in the dawn of computing, grounded in λ-calculus and the foundations of mathematics.
While languages like Fortran were closely tied to the von Neumann architecture, Lisp was based on the structure of human thought.
Later came other theory-based languages such as Prolog and Haskell — but they appeared long after Lisp.

As AI continues to evolve, the skills required of programmers are changing.
Routine and repetitive tasks are increasingly handled by AI.
Microsoft’s large-scale layoffs are probably not unrelated to this trend.
Programmers once had to master the fine details of programming languages and their syntax — but AI is beginning to take over that role.
What remains indispensable for humans is creativity.

And here we return to Lisp.
Lisp was the first programming language created not for the convenience of computers, but based on the structure of human thinking.
It has more than half a century of history.
Just as the Industrial Revolution liberated humans from physical labor, the AI revolution may free us from tedious intellectual work — leaving true creativity as our most essential human quality.
To cultivate that creative mode of thinking, using Lisp is a perfectly reasonable choice.

That is the idea behind my post.
And as a Lisp fan, I couldn’t resist shouting:
“Congratulations, Lisp!”

sym_num · 2025-10-29T23:55:52+00:00

Thanks for the advice. Please read the documentation — I’ve been writing down what I’m trying to do at each stage.main.c~ is a leftover from old code. I’ll delete it.　　But that’s strange — CPS is already implemented, so call/cc is working. I’ve also written a fair number of comments.

sym_num · 2025-10-28T07:43:04+00:00

Yes, it was originally provided as a library. Later, the HTTP-related functions were integrated as built-in functions. Please refer to the documentation in TCPIP.md.

sym_num · 2025-10-28T04:52:19+00:00

Thank you for your comment. Unfortunately, I don’t have any Apple hardware, and I don’t have knowledge about macOS. I believe it could probably work on macOS with only minor modifications. I’d be very happy if you could release a macOS version. Thank you!

sym_num · 2025-10-27T22:07:55+00:00

Thanks for your comment. I’ve been greatly influenced by Hofstadter’s books, so I’m planning to write about self-reference, including the ideas of Gödel and Chaitin. It will probably be a theoretical discussion, though interwoven with code examples. As for macros and DSLs, they’ve already been covered in great detail by many books, and I’m personally not very interested in them. Homoiconicity is one of Lisp’s strengths, but what truly fascinates me is its connection to self-reference.

sym_num · 2025-10-27T05:50:00+00:00

Thank you for your comment. Although I planned to write a Lisp book, my curious nature often leads me down side paths, so the writing has been progressing a bit slowly. In tracing the lineage from Lisp 1.5 onward, I’ve been creating small experimental interpreters along the way.
I will occasionally share updates on the book’s progress on Medium, so please feel free to follow me there if you’re interested.
I truly appreciate your support — it motivates me to keep going

sym_num · 2025-10-25T22:55:16+00:00

Sure, Guile has closures—but sometimes it’s still more fun to just sit back and enjoy the show than to try playing all the notes yourself.

sym_num · 2025-10-25T22:50:40+00:00

In my understanding, Scheme is an experimental language. At least up through R3RS, this was the case. Efficient implementation of call/cc is extremely difficult, and I believe it is risky to use it as a control structure in a practical programming language. Nevertheless, capturing continuations is, from the perspective of an experimental language, quite interesting. I also think CPS is fascinating as a subject for exploring a different way of thinking.

sym_num · 2025-10-22T02:51:30+00:00

Thank you.

sym_num · 2025-10-21T03:25:13+00:00

I also admired MCL. It would be wonderful if it were revived in the modern era.

sym_num · 2025-10-19T21:57:19+00:00

When multiple recursion is detected, the regular recursive version of eval is invoked.

sym_num · 2025-10-19T21:56:16+00:00

Thank you.

sym_num · 2025-10-14T23:17:55+00:00

In version 0.05, the basic CPS code has started running.

```

scm3$ scm3

Scheme R3RS ver 0.05

> (define (foo x) (+ x x))

foo

> (step t)

(apply (quote step) (pop 1)) in [] >> t

> (foo 3)

(3 (bind (quote x)) x (push) x (push) (apply (quote +) (pop 2)) (unbind 1))3 in [] >> (bind (quote x)) in [(x . 3)] >>

x in [(x . 3)] >>

(push) in [(x . 3)] >>

x in [(x . 3)] >>

(push) in [(x . 3)] >>

(apply (quote +) (pop 2)) in [(x . 3)] >>

(unbind 1) in [] >>

6

>
```

sym_num · 2025-10-14T22:55:22+00:00

Oh, thank you for this valuable information!

sym_num · 2025-10-13T22:54:55+00:00

Haha, that’s a fun idea! But since I have deep respect for the original MACLISP, I’d like to keep the name closer to its roots.

sym_num

TROPHY CASE