I've formalized basics of Prolog in Coq to have 100% understanding

General
1
  1. I’ve used only a small subset of Coq type theory: Calculus of Constructions with Definitions (λD) as defined in the textbooks. It is clean, simple and strong enough to express all mathematics in it
  2. Calculus of Constructions allows you to derive all mathematics from pure logic and let you formalize Natural Deduction. It is a very natural idea to fit logical programming in.
  3. The main goal is education, learning and deep understanding. It is very helpful to reconnect prolog with the foundations of mathematics
  4. I defined Axiom Term: Type to express the idea of Prolog term and Axiom kb: Term->Prop to reconnect a term with the fact that it belongs to our knowledge base
  5. Complex terms defined as predicates on other terms
  6. Numbers and lists are defined from scratch as pure terms
  7. Variables expressed as universal quantification variables, not as a special term type
  8. I’ve added notations for lists, numbers and also a special notation to insert Prolog code directly into Coq source (~ code ~)
  9. There is no automatic unification and proof search. You must do it by yourself step by step while proving your goal as a theorem. It is super helpful for learning and understanding
  10. I’ve covered most key points and exercises from 6 chapters of “Learn Prolog Now” course
Axiom append: Term -> Term -> Term -> Term.
Axiom append_base: ∀L. ~ append [] L L ~.
Axiom append_rec: ∀A. ∀B. ∀H. ∀T. ~ append [H|T] A [H|B] :- append T A B ~.

Goal ~append [mia] [yolanda] [mia, yolanda]~.
apply append_rec.
apply append_base.
Qed.

Check it out https://github.com/kciray8/the-great-formalization-project/blob/425fd68e632727177d0cdfdb2b0c6b73571726e4/textbooks/learn-prolog-now/Chapters.v

1 Like