Resolution Methods in Proving the Program Correctness
Branko Markoski, Petar Hotomski, Dušan Malbaški, Danilo Obradović (2007)
The Yugoslav Journal of Operations Research
Similarity:
Branko Markoski, Petar Hotomski, Dušan Malbaški, Danilo Obradović (2007)
The Yugoslav Journal of Operations Research
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...
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...
Branko Markoski, Petar Hotomski, Dušan Malbaški, Danilo Obradović (2010)
The Yugoslav Journal of Operations Research
Similarity:
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...
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...
Milenko Mosurović, Tatjana Stojanović, Ana Kaplarević-Mališić (2009)
Zbornik Radova
Similarity:
Gérard Milhaud, Élisabeth Godbert (1998)
Mathématiques et Sciences Humaines
Similarity:
We present a system providing a set of tools for developing natural language processing (NLP) applications such as natural language interfaces, communication aid systems, etc. This system is based on two principles: modularity of knowledge representation to ensure the portability of the system, and guided sentence composition to ensure transparency, i.e. to ensure that the produced sentences are well-formed at the lexical, syntactic, semantic and conceptual levels. We first describe...
Prešić, Slaviša B. (1997)
Publications de l'Institut Mathématique. Nouvelle Série
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:
Radev, Slavian (2007)
Serdica Journal of Computing
Similarity:
In the present paper we investigate the life cycles of formalized theories that appear in decision making instruments and science. In few words mixed theories are build in the following steps: Initially a small collection of facts is the kernel of the theory. To express these facts we make a special formalized language. When the collection grows we add some inference rules and thus some axioms to compress the knowledge. The next step is to generalize these rules to all expressions in...