Displaying similar documents to “Taclets: a new paradigm for constructing interactive theorem provers.”

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

Grounding and extracting modal responses in cognitive agents: 'AND' query and states of incomplete knowledge

Radosław Katarzyniak, Agnieszka Pieczynska-Kuchtiak (2004)

International Journal of Applied Mathematics and Computer Science

Similarity:

In this study an original way of modeling language grounding and generation for a simple set of language responses is presented. It is assumed that the language is used by a cognitive agent and consists of a few modal belief and possibility formulas that are used by this agent to communicate its opinions on the current state of an object. The cognitive agent is asked a simple AND query and the language is tailored to this situation. The agent's knowledge bases are characterized by certain...

On some properties of grounding nonuniform sets of modal conjunctions

Radoslaw Katarzyniak (2006)

International Journal of Applied Mathematics and Computer Science

Similarity:

A language grounding problem is considered for nonuniform sets of modal conjunctions consisting of conjunctions extended with more than one modal operator of knowledge, belief or possibility. The grounding is considered in the context of semiotic triangles built from language symbols, communicative cognitive agents and external objects. The communicative cognitive agents are assumed to be able to observe external worlds and store the results of observations in internal knowledge bases....

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