• English only

# Differences

This shows you the differences between two versions of the page.

 sav08:theorem_prover [2008/02/20 10:31]vkuncak sav08:theorem_prover [2008/02/21 09:47] (current)vkuncak Both sides previous revision Previous revision 2008/02/21 09:47 vkuncak 2008/02/20 10:31 vkuncak 2008/02/20 10:30 vkuncak 2008/02/20 10:23 vkuncak 2008/02/20 10:09 vkuncak 2008/02/20 09:22 vkuncak 2008/02/20 09:21 vkuncak 2008/02/18 17:00 vkuncak 2008/02/18 16:55 vkuncak 2008/02/18 16:35 vkuncak 2008/02/18 16:25 vkuncak created 2008/02/21 09:47 vkuncak 2008/02/20 10:31 vkuncak 2008/02/20 10:30 vkuncak 2008/02/20 10:23 vkuncak 2008/02/20 10:09 vkuncak 2008/02/20 09:22 vkuncak 2008/02/20 09:21 vkuncak 2008/02/18 17:00 vkuncak 2008/02/18 16:55 vkuncak 2008/02/18 16:35 vkuncak 2008/02/18 16:25 vkuncak created Line 25: Line 25: Example: ​ Example: ​ * [[Isabelle Theorem Prover]] * [[Isabelle Theorem Prover]] - * [[http://​pauillac.inria.fr/​coq/​|Coq Proof Assistant]] + * [[http://​pauillac.inria.fr/​coq/​|Coq Proof Assistant]] ​- popular in programming languages community - * [[http://​www.cs.utexas.edu/​~moore/​acl2/​|ACL2 Language and Prover]] + * [[http://​www.cs.utexas.edu/​~moore/​acl2/​|ACL2 Language and Prover]] ​- identifies a LISP subset with a logic === Decision Procedure === === Decision Procedure === - It considers a smaller set of formulas, it always terminates and (given enough time) never says "I don't know". + Decision procedure ​considers a smaller set of formulas, it always terminates and (given enough time) never says "I don't know". Example decidable classes of formulas: Example decidable classes of formulas:

sav08/theorem_prover.txt · Last modified: 2008/02/21 09:47 by vkuncak

© EPFL 2018 - Legal notice