Displaying similar documents to “Repetitions and permutations of columns in the semijoin algebra”

From two- to four-valued logic

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.

Towards specifying with inclusions.

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...

Cocktail: a tool for deriving correct programs.

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...

Some key research problems in automated theorem proving for hardware and software verification.

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...