Reasoning in Basic Description Logics and Description Logics with Modal Operators
Milenko Mosurović, Tatjana Stojanović, Ana Kaplarević-Mališić (2009)
Zbornik Radova
Similarity:
Milenko Mosurović, Tatjana Stojanović, Ana Kaplarević-Mališić (2009)
Zbornik Radova
Similarity:
Barbara Dunin-Kęplicz, Linh Anh Nguyen, Andrzej Sza l as (2010)
Computer Science and Information Systems
Similarity:
Radosław Klimek (2014)
International Journal of Applied Mathematics and Computer Science
Similarity:
Chris Brink (1993)
Banach Center Publications
Similarity:
The purpose of this note is to show that a known and natural four-valued logic co-exists with classical two-valued logic in the familiar context of truth tables. The tool required is the power construction.
Luigia Aiello, Mario Aiello, Giuseppe Attardi, Gianfranco Prini (1976)
Annales scientifiques de l'Université de Clermont. Mathématiques
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...
L. Banachowski, A. Kreczmar, G. Mirkowska, H. Rasiowa, A. Sławicki (1977)
Banach Center Publications
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...
Rudolf Berghammer, Gunther Schmidt (1993)
Banach Center Publications
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...