Logic and Foundations
A proof-assistant is a computer program with which a user can construct completely formal mathematical proofs in some kind of logical system. In contrast to a theorem prover, a proof-assistant cannot find proofs on its own
LF Logical Framework
The Edinburgh Logical Framework is, with De Bruijn's AUTOMATH, one of the two most influential implemented proof representation systems in existence.
Copyright © 1998-2016 AOL Inc.
Last update: Sunday, September 6, 2015 6:24:02 AM EDT -