1,721,260 research outputs found
Program Tactics and Logic Tactics
No full textA tactic is any procedure which implements a correct search strategy. The goal of this paper is to provide a uniform framework where the user can hand-code tactics as programs in a metalevel programming language, can theorem prove them as terms in a first order classical metatheory, and is provided with a mechanism which allows for a bidirectional `translation` between the programming language and the logic. We call tactics of the first kind, `Program tactics`, those of the second kind `Logic tactics`. Inside this framework it is possible to use program tactics as terms inside Logic tactics and, viceversa, to use Logic tactics as programs inside Program tactic
Planning as Model Checking for Extended Goals in Non-deterministic Domains
No full textRecent research has addressed the problem of planning in non-deterministic domains. Classical planning has also been extended to the case of goals that can express temporal properties. However, the combination of these two aspects is not trivial. In non-deterministic domains, goals should take into account the fact that a plan may result in many possible different executions and that some requirements can be enforced on all the possible executions, while others may be enforced only on some executions. In this paper we address this problem. We define a planning algorithm that generates automatically plans for extended goals in non-deterministic domains, and prove that the algorithm is correct and complete. We provide an implementation of the planning algorithm by using symbolic model checking techniques, and show that it is effective in practice with some experimental result
A metatheory of a mechanized object theory
No full textAbstractIn this paper we propose a metatheory, MT, which represents the computation which implements its object theory, OT, and, in particular, the computation which implements deduction in OT. To emphasize this fact we say that MT is a metatheory of a mechanized object theory. MT has some “unusual” properties, e.g. it explicitly represents failure in the application of inference rules, and the fact that large amounts of the code implementing OT are partial, i.e. they work only for a limited class of inputs. These properties allow us to use MT to express and prove tactics, i.e. expressions which specify how to compose possibly failing applications of inference rules, to interpret them procedurally to assert theorems in OT, to compile them into the system implementation code, and, finally, to generate MT automatically from the system code. The definition of MT is part of a larger project which aims at the implementation of self-reflective systems, i.e. systems which are able to introspect their own code, to reason about it and, possibly, to extend or modify it
Mechanized Result Verification: an Industrial Application
No full textWe present part of an industrial project where mechanized theorem proving is used for the validation of a translator which generates safety critical software. In this project, the mechanized proof is decomposed in two parts: one is done `on-line`, at each run of the translator, by a custom prover which checks automatically that the result of each translation meets some verification conditions; the other is done `off-line`, once for all, interactively with a general purpose prover; the off-line proof shows that the verification conditions checked by the on-line prover are sufficient to guarantee the correctness of each translation. The provably correct verification conditions can thus be seen as specifications for the on-line prover. This approach is called mechanized result verificatio
- …
