PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 4

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  automated theorem proving
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Proving Theorems by Program Transformation
Fioravanti F., Pettorossi A., Proietti M., Senni V.
Fundamenta Informaticae
|
2013
|
Vol. 127, nr 1-4
115--134
EN
In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.
2
Content available remote Methods of knowledge representation and processing in control of intelligent tutoring systems
Vassilyev S. N., Smirnova N. V., Sukonnova A. A., Shvarts A. Yu.
Management and Production Engineering Review
|
2011
|
Vol. 2, No. 3
71-84
EN
The paper is dedicated to methods of increasing the intelligence level of interactive tutoring systems. New logical methods of knowledge representation and processing with application in intelligent control of tutoring systems are considered. The proposed methods are useful in problems which require coupling logics and heuristics as well as in problems with incomplete information and have other specifics in comparison with known intelligent components of computer systems. The architecture of a concrete intelligent tutoring system "Volga" is considered. The methods of automation of course tasks solving and action planning as well as techniques of constructing student's model are proposed.
3
Content available remote Automation for Dependently Typed Functional Programming
Wilson S., Fleuriot J., Smaill A.
Fundamenta Informaticae
|
2010
|
Vol. 102, nr 2
209-228
EN
Writing dependently typed functional programs that capture non-trivial program properties is difficult in current systems due to lack of proof automation. We identify proof patterns that occur when programming with dependent types and detail how automating such patterns allow us to work more comfortably with types that capture, for example, membership, ordering and nonlinear arithmetic properties. We describe the role of the rippling heuristic, both for inductive and non-inductive proofs, and generalisation in providing such automation. We then discuss an implementation of our ideas in Coq with practical examples of dependently typed programs, that capture useful program properties, which can be verified automatically. We demonstrate that our proof automation is generic in that it can provide support for working with theorems involving user-defined functions and inductive data types.
4
Content available remote Towards automated consistency checking of module interface specifications
Engel M., Kret A., Mincer-Daszkiewicz J.
Fundamenta Informaticae
|
2000
|
Vol. 42, nr 3,4
251-278
EN
The Trace Assertion Method (TAM) pioneered by Parnas is a formalism used to specify software module interfaces. The main purpose of the research described in this paper is to recognize the possibilities of linking the TAM editor with one of the existing theorem proving systems and to enable thereby the automated consistency checking of trace specifications. Possible approaches to embedding TAM in the Prototype Verification System (PVS) specification language are discussed and the chosen shallow definitional embedding is described in detail. Proof obligations for the consistency checking of trace specifications are obtained as type correctness conditions generated automatically by the PVS type checker. Some of these obligations can be proven automatically by PVS, other proofs need human guidance. Possible ways of increasing automation capabilities of the PVS theorem prover are recognized and presented. We share our experience in defining both specialized and general purpose proof strategies. This research may be viewed as a case study in applying the existing general purpose proof system to consistency checking of some application-specific formalism, which might be of interest for the software designer community
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.