The Coq mailing list

[Dominik Kirst <kirst AT ps.uni-saarland.de>]

Hi Alex,

Herbelin and Lee have formalised the first-order sequent calculus LJT in Coq (https://hal.inria.fr/inria-00381554/document). In a current draft (http://www.ps.uni-saarland.de/~kirst/drafts/paper.pdf) we report on Coq formalisations of the completeness of LJT as well as a more conventional first-order sequent calculus LJ. Both are deep embeddings in the sense of the first article you mentioned and we have used a de Bruijn encoding of binders. 

Hope this helps,

Dominik

-----------------------------------------
Programming Systems Lab
Saarland University
http://www.ps.uni-saarland.de/~kirst/

On 8. Sep 2019, at 16:22, Alex Meyer <alex153 AT outlook.lv> wrote:

Hi!

I am a bit confused about doing logic in Coq and about availability of the sequent calculus (Gentzen or Hilber, anyway) for full first order logic in Coq. Google gives articles about sequent calculus for porpositional logic in Coq, but I have not managed to find one for first order.

There are two notes:

/1. Sequent calculus for other logics (with variables - first order) have already be done e.g. in https://www.sciencedirect.com/science/article/pii/S157106611830080X "Mechanizing Focused Linear Logic in Coq" - in that article the set of rules is formalized as inductive type with constructor for each rule (for sequents). So, it is not easy, but it can be done - one should simply transfer this approach for the sequent rules that have been written on the paper for already decades of years. Well, such approach involves handling of variables and binding and HOAS - higher order (parametric) abstract syntax. Maybe that has prohibited to develop FOL sequent calculus in Coq so far?

/2. Article https://arxiv.org/abs/1905.09381 "Learning to Prove Theorems via Interacting with Proof Assistants" gives high level overview of Coq approach: every theorem can be proved in low level manner - by encoding it in logical statement and solving the SAT problem for the negation of that statement. Coq, it is said in that article, is higher level approach that does not try to cast everything in the logical level, but that tries to use higher level notions, concepts (that, of course can be expressed in the low level logical definitions) and theorems in higher level reasoning. So, such viewpoint can invalidate the need for sequent calculus in Coq.

But, I guess, there are lot of tasks that requires doing logic in low level manner. E.g. almost all knowledge bases, knowledge graphs in exper systems are expressed as logical formulas, so, one is eager to apply Coq in such expert systems as well and that is why sequent calculus may be needed.

This my question is connected with the previous question https://sympa.inria.fr/sympa/arc/coq-club/2019-09/msg00027.html about use of Coq for forward chaining/reasoning/inference. Formalization of sequent calculus for FOL is requirement, I guess, for doing such forward inference.

https://content.sciendo.com/view/journals/ausi/8/1/article-p41.xml "Contralog: a Prolog conform forward-chaining environment and its application for dynamic programming and natural language parsing" is example how forward inference is being enabled in Prolog, that is as backward inference intended systams as Coq is. Maybe that can give some inspiration.

Thanks,

Alex

Attachment: signature.asc
Description: Message signed with OpenPGP