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:
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
Luigia Aiello, Mario Aiello, Giuseppe Attardi, Gianfranco Prini (1976)
Annales scientifiques de l'Université de Clermont. Mathématiques
Similarity:
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...
Adam Meissner (2011)
International Journal of Applied Mathematics and Computer Science
Similarity:
A computation rule determines the order of selecting premises during an inference process. In this paper we empirically analyse three particular computation rules in a tableau-based, parallel reasoning system for the ALC description logic, which is built in the relational programming model in the Oz language. The system is constructed in the lean deduction style, namely, it has the form of a small program containing only basic mechanisms, which assure soundness and completeness of reasoning....
Andrzej Pułka (2014)
International Journal of Applied Mathematics and Computer Science
Similarity:
Andrzej Pułka (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:
Predrag Janičić (2012)
Review of the National Center for Digitization
Similarity:
Luis M. Laita, Roanes-Lozano, Luis De Ledesma Otamendi (2007)
RACSAM
Similarity:
In this paper, the questions of what machines cannot do and what they can do will be treated by examining the ideas and results of eminent mathematicians. Regarding the question of what machines cannot do, we will rely on the results obtained by the mathematicians Alan Turing and Kurt G¨odel. Turing machines, their purpose of defining an exact definition of computation and the relevance of Church-Turing thesis in the theory of computability will be treated in detail. The undecidability...
Radosław Klimek (2014)
International Journal of Applied Mathematics and Computer Science
Similarity:
Grzegorz J. Nalepa, Antoni Ligęza (2010)
International Journal of Applied Mathematics and Computer Science
Similarity:
This paper describes a new approach, the HeKatE methodology, to the design and development of complex rule-based systems for control and decision support. The main paradigm for rule representation, namely, eXtended Tabular Trees (XTT), ensures high density and transparency of visual knowledge representation. Contrary to traditional, flat rule-based systems, the XTT approach is focused on groups of similar rules rather than on single rules. Such groups form decision tables which are connected...
Branko Markoski, Petar Hotomski, Dušan Malbaški, Danilo Obradović (2007)
The Yugoslav Journal of Operations Research
Similarity: