Journal of Automated Reasoning
Công bố khoa học tiêu biểu
* Dữ liệu chỉ mang tính chất tham khảo
Sắp xếp:
A Formally Verified Compiler Back-end
Journal of Automated Reasoning - Tập 43 - Trang 363-446 - 2009
This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its soundness. Such a verified compiler is useful in the context of formal methods applied to the certification of crit...... hiện toàn bộ
Guarded Cubical Type Theory
Journal of Automated Reasoning - Tập 63 - Trang 211-253 - 2018
This paper improves the treatment of equality in guarded dependent type theory (
$$\mathsf {GDTT}$$
), by combining it with cubical type theory (
$$\mathsf {CTT}$$
...... hiện toàn bộ
Proving Divide and Conquer Complexities in Isabelle/HOL
Journal of Automated Reasoning - Tập 58 - Trang 483-508 - 2016
The Akra–Bazzi method (Akra and Bazzi in Comput Optim Appl 10(2):195–210, 1998. doi:
10.1023/A:1018373005182
), a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide and Conquer algorithms. This work describes a formalisation of the Akra–Bazzi method (as generalised by Leighton in Notes on bet...... hiện toàn bộ
Long-Distance Q-Resolution with Dependency Schemes
Journal of Automated Reasoning - Tập 63 - Trang 127-155 - 2018
Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers that use these systems to generate proofs. We study a combination of two proof systems supported by the solver DepQBF: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We sh...... hiện toàn bộ
Clifford Algebraic Reduction Method for Automated Theorem Proving in Differential Geometry
Journal of Automated Reasoning - Tập 21 - Trang 1-21 - 1998
In this paper a new method is proposed for mechanically proving theorems in the local theory of space curves. The method is based on Ritt-Wu’s well-ordering principle of ordinary differential polynomials, Clifford algebraic representation of Euclidean space and equation set solving in Clifford algebra formalism. It has been tested by various theorems and seems to be efficient.
A Compendium of Continuous Lattices in MIZAR
Journal of Automated Reasoning - Tập 29 - Trang 189-224 - 2002
This paper reports on the MIZAR formalization of the theory of continuous lattices as presented in Gierz et al.: A Compendium of Continuous Lattices, 1980. By a MIZAR formalization we mean a formulation of theorems, definitions, and proofs written in the MIZAR language whose correctness is verified by the MIZAR processor. This effort was originally motivated by the question of whether or not the M...... hiện toàn bộ
The problem of choosing the type of subsumption to use
Journal of Automated Reasoning - - 1991
This article is the eighteenth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria for choosing the type of subsumption (if any) to use for completing a specific assignment. Since subsumption can be expensive (in terms of computer time), the application of such criteria to select the most effective va...... hiện toàn bộ
Verifying Termination and Reduction Properties about Higher-Order Logic Programs
Journal of Automated Reasoning - Tập 34 - Trang 179-207 - 2006
We describe two checkers for verifying termination and reduction properties about higher-order logic programs. The reduction checker verifies that the result of a program execution is structurally smaller than (or equal to) the inputs to the program. The termination checker guarantees that the inputs of the recursive calls are structurally smaller than the inputs of the original call, taking into...... hiện toàn bộ
Hierarchical deduction
Journal of Automated Reasoning - Tập 3 - Trang 35-77 - 1987
This paper describes an hierarchical deduction proof procedure. This procedure proves a theorem by searching for a proof acceptable to an hierarchical deduction structire; those derivations which are irrelevant to this proof are limited by means of a set of completeness-preserving refinements of the basic procedure, such as constraints on framed literals and on common tails, a proper reduction ref...... hiện toàn bộ
Tổng số: 936
- 1
- 2
- 3
- 4
- 5
- 6
- 10