- 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
- 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.
- The main goal is education, learning and deep understanding. It is very helpful to reconnect prolog with the foundations of mathematics
- 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
- Complex terms defined as predicates on other terms
- Numbers and lists are defined from scratch as pure terms
- Variables expressed as universal quantification variables, not as a special term type
- I’ve added notations for lists, numbers and also a special notation to insert Prolog code directly into Coq source (~ code ~)
- 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
- 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