Displaying similar documents to “What machines can and cannot do.”

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

The role of heuristics in automated theorem proving. J.A. Robinson's resolution principle.

Roberto Cordeschi (1996)

Mathware and Soft Computing

Similarity:

The aim of this paper is to show how J.A. Robinson's resolution principle was perceived and discussed in the AI community between the mid sixties and the first seventies. During this time the so called heuristic search paradigm was still influential in the AI community, and both resolution principle and certain resolution based, apparently human-like, search strategies were matched with those problem solving heuristic procedures which were representative of the AI heuristic search paradigm. ...

An abstract monadic semantics for value recursion

Eugenio Moggi, Amr Sabry (2004)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök...

Termination checking with types

Andreas Abel (2004)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces Λ μ + , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose...