Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:theorem_prover [2008/02/20 10:31]
vkuncak
sav08:theorem_prover [2008/02/21 09:47] (current)
vkuncak
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