Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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