coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Intuition Tactic

From: david.delahaye AT cnam.fr
To: "t x" <txrev319 AT gmail.com>
Cc: "coq-club" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Intuition Tactic
Date: Sat, 5 Oct 2013 09:45:09 +0200
Importance: Normal

Hi,

> Thus, my question: what algorithm can be used to solve propositional
> logic in Coq?

You can use the proof search algorithm of the tauto tactic, which is actually
based on the contraction-free sequent calculi LJT* of Roy Dyckhoff. This
algorithm is purely syntactical and implements directly the deduction rules of
the system with a point of backtracking when the rule is not invertible (in
this system, only two rules are not invertible).

Best regards,

David.

--------------------------------------
David Delahaye,
David.Delahaye AT cnam.fr
http://cedric.cnam.fr/~delahaye/

[Coq-Club] Intuition Tactic, t x, 10/04/2013
- Re: [Coq-Club] Intuition Tactic, AUGER Cédric, 10/04/2013
- Re: [Coq-Club] Intuition Tactic, david . delahaye, 10/05/2013