Structured theory development for a mechanized logic (Q1595929)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Structured theory development for a mechanized logic |
scientific article; zbMATH DE number 1565456
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Structured theory development for a mechanized logic |
scientific article; zbMATH DE number 1565456 |
Statements
Structured theory development for a mechanized logic (English)
0 references
18 February 2001
0 references
Several aspects concerning the structuring mechanisms for the ACL2 (A Computational Logic for Applicative Common Lisp) theorem prover are presented in this paper. A brief overview of ACL2 is realized. Two notions of admissibility for recursive definitions are introduced. The notion of ACL2 history is introduced and this notion formalizes the result of a user's interaction with ACL2. The theorems of a chronology are consequences of its axioms.
0 references
first-order logic
0 references
automated reasoning
0 references
ACL2
0 references
constraint
0 references
encapsulation
0 references
functional instantiation
0 references
soundness
0 references
