Informal proofs formally checked by machine
Luigia Aiello, Mario Aiello, Giuseppe Attardi, Gianfranco Prini (1976)
Annales scientifiques de l'Université de Clermont. Mathématiques
Similarity:
Luigia Aiello, Mario Aiello, Giuseppe Attardi, Gianfranco Prini (1976)
Annales scientifiques de l'Université de Clermont. Mathématiques
Similarity:
Branko Markoski, Petar Hotomski, Dušan Malbaški, Danilo Obradović (2007)
The Yugoslav Journal of Operations Research
Similarity:
Michael Franssen, Harrie De Swart (2004)
RACSAM
Similarity:
Cocktail is a tool for deriving correct programs from their specifications. The present version is powerful enough for educational purposes. The tool yields support for many sorted first order predicate logic, formulated in a pure type system with parametric constants (CPTS), as the specification language, a simple While-language, a Hoare logic represented in the same CPTS for deriving programs from their specifications and a simple tableau based automated theorem prover for verifying...
Matt Kaufmann, J. Strother Moore (2004)
RACSAM
Similarity:
This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In...
Vojislav B. Mišić, Dušan M. Velašević (1997)
The Yugoslav Journal of Operations Research
Similarity:
Milenko Mosurović, Tatjana Stojanović, Ana Kaplarević-Mališić (2009)
Zbornik Radova
Similarity:
Radosław Klimek (2014)
International Journal of Applied Mathematics and Computer Science
Similarity:
Barbara Dunin-Kęplicz, Linh Anh Nguyen, Andrzej Sza l as (2010)
Computer Science and Information Systems
Similarity:
Giovanni Criscuolo (1996)
Mathware and Soft Computing
Similarity:
Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, Steffen Schlager (2004)
RACSAM
Similarity:
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...
Jaume Agustí, Jordi Puigsegur, W. Marco Schorlemmer (1997)
Mathware and Soft Computing
Similarity:
In this article we present a functional specification language based on inclusions between set expressions. Instead of computing with data individuals we deal with their classification into sets. The specification of functions and relations by means of inclusions can be considered as a generalization of the conventional algebraic specification by means of equations. The main aim of this generalization is to facilitate the incremental refinement of specifications. Furthermore, inclusional...