Computer Science – Logic in Computer Science
Scientific paper
2000-10-31
Journal of Automated Reasoning 5 (1989), 363-397
Computer Science
Logic in Computer Science
Scientific paper
Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in which the object-logics are formalized. Isabelle is now based on higher-order logic -- a precise and well-understood foundation. Examples illustrate use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment. Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet's higher-order unification procedure.
No associations
LandOfFree
The Foundation of a Generic Theorem Prover does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with The Foundation of a Generic Theorem Prover, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The Foundation of a Generic Theorem Prover will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-446301