Search: WFRF:(Hähnle Reiner 1962) >
Taclets: a new para...
Taclets: a new paradigm for writing theorem provers : Taclets: Un nuevo paradigma para construir demostradores automáticos interactivos
-
Beckert, Bernhard (author)
-
Giese, Martin, 1970 (author)
-
Habermalz, Elmar (author)
-
show more...
-
Hähnle, Reiner, 1962 (author)
-
Roth, Andreas (author)
-
- Rümmer, Philipp, 1978 (author)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap (GU),Department of Computer Science and Engineering, Computing Science (GU)
-
Schlager, Steffen (author)
-
show less...
-
(creator_code:org_t)
- 2004
- 2004
- English.
-
In: REVISTA DE LA REAL ACADEMIA DE CIENCIAS, Serie A: Matemáticas. - 1578-7303. ; 98:1, s. 17-53
- Related links:
-
https://gup.ub.gu.se...
Abstract
Subject headings
Close
- Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules of calculi have not only purely logical content, but contain restrictions on the expected context of rule applications and heuristic information. We suggest a new and minimalist concept for implementing interactive theorem provers called taclet. Their usage can be mastered in a matter of hours, and they are efficiently compiled into the GUI of a prover. We implemented the KeY system, an interactive theorem prover for the full JavaCard language based on taclets.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Keyword
- logic
- theorem proving
- interactive theorem proving
Publication and Content Type
- ref (subject category)
- art (subject category)
Find in a library
To the university's database
- By the author/editor
-
Beckert, Bernhar ...
-
Giese, Martin, 1 ...
-
Habermalz, Elmar
-
Hähnle, Reiner, ...
-
Roth, Andreas
-
Rümmer, Philipp, ...
-
show more...
-
Schlager, Steffe ...
-
show less...
- About the subject
-
- NATURAL SCIENCES
-
NATURAL SCIENCES
-
and Computer and Inf ...
- Articles in the publication
-
REVISTA DE LA RE ...
- By the university
-
University of Gothenburg