The search session has expired. Please query the service again.

The search session has expired. Please query the service again.

Displaying similar documents to “Some key research problems in automated theorem proving for hardware and software verification.”

The HeKatE methodology. Hybrid engineering of intelligent systems

Grzegorz J. Nalepa, Antoni Ligęza (2010)

International Journal of Applied Mathematics and Computer Science

Similarity:

This paper describes a new approach, the HeKatE methodology, to the design and development of complex rule-based systems for control and decision support. The main paradigm for rule representation, namely, eXtended Tabular Trees (XTT), ensures high density and transparency of visual knowledge representation. Contrary to traditional, flat rule-based systems, the XTT approach is focused on groups of similar rules rather than on single rules. Such groups form decision tables which are connected...

Contexts, locality and generality.

Paolo Bouquet, Enrico Giunchiglia, Fausto Giunchiglia (1996)

Mathware and Soft Computing

Similarity:

It has been recognized that AI programs suffer from a lack of generality, the first gross symptom being that a small variation to the problem being solved usually causes a major revision of the theory describing it. The lack of generality seems an unavoidable consequence of the process of approximating the world while building theories about it. In this paper we propose an approach where generality is achieved by formulating, for each problem at hand, an appropriate local theory, a theory...

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

Taclets: a new paradigm for constructing interactive theorem provers.

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

What machines can and cannot do.

Luis M. Laita, Roanes-Lozano, Luis De Ledesma Otamendi (2007)

RACSAM

Similarity:

In this paper, the questions of what machines cannot do and what they can do will be treated by examining the ideas and results of eminent mathematicians. Regarding the question of what machines cannot do, we will rely on the results obtained by the mathematicians Alan Turing and Kurt G¨odel. Turing machines, their purpose of defining an exact definition of computation and the relevance of Church-Turing thesis in the theory of computability will be treated in detail. The undecidability...