coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Decision Procedure of Two-Variable First order logic in Coq

From: "Randy For Coq" <randycoq AT 163.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Decision Procedure of Two-Variable First order logic in Coq
Date: Sun, 13 Oct 2013 09:24:05 +0800 (CST)

hi all, is there any previous work on verifying the decision procedure for two-variable FOL in Coq ? If no, can you recommend some paper having detailed description of the procedure? Thank you all very much!

[Coq-Club] Decision Procedure of Two-Variable First order logic in Coq, Randy For Coq, 10/13/2013