首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   20篇
  完全免费   3篇
  自动化技术   23篇
  2017年   2篇
  2015年   1篇
  2013年   1篇
  2011年   1篇
  2010年   1篇
  2009年   2篇
  2008年   2篇
  2007年   5篇
  2006年   4篇
  2003年   1篇
  2002年   2篇
  1997年   1篇
排序方式: 共有23条查询结果,搜索用时 31 毫秒
1.
We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case. In our nominal approach, alpha-equality of lambda terms coincides with Coq's built-in equality. Our axiomatization includes a nominal induction principle and functions for calculating free variables and substitution. These axioms are collected in a module signature and proved sound using locally nameless terms as the underlying representation. Our experience so far suggests that it is feasible to work from such axiomatized theories in Coq and that the nominal style of variable binding corresponds closely with paper proofs. We are currently working on proving the soundness of a primitive recursion combinator and developing a method of generating these axioms and their proof of soundness from a grammar describing the syntax of terms and binding.  相似文献
2.
We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler implementations, and we point out that much can be done without binders or alpha-conversion. We propose specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.  相似文献
3.
We propose a decision procedure for algebraically closed fields based on a quantifier elimination method. The procedure is intended to build proofs for systems of polynomial equations and inequations. We describe how this procedure can be carried out in a proof assistant using a Computer Algebra system in a purely skeptical way. We present an implementation in the particular framework of Coq and Maple giving some details regarding the interface between the two tools. This allows us to show that a Computer Algebra system can be used not only to bring additional computational power to a proof assistant but also to enhance the automation of such tools.  相似文献
4.
5.
We present in this paper the design of a graphical user interface to deal with proofs in geometry. The software developed combines three tools: a dynamic geometry software to explore, measure, and invent conjectures; an automatic theorem prover to check facts; and an interactive proof system (Coq) to mechanically check proofs built interactively by the user.  相似文献
6.
This article presents the design of a new functional 2D image segmentation algorithm by cell merging in a subdivision, its proof of total correctness, and the derivation of an optimal imperative program. The planar subdivisions are modeled by hypermaps. The formal specifications of hypermaps and segmentation are developed in the Calculus of Inductive Constructions. The proofs are assisted by the Coq system. The final program is written in C.  相似文献
7.
This paper presents a formalization in Coq of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.   相似文献
8.
The paper describes the general philosophy and the main architectural and technological solutions adopted in the HELM Project for the management of large repositories of mathematical knowledge. The leitmotiv is the extensive use of XML technology, and the exploitation of information in the Web way, that is without a central authority, with few basic rules, in a scalable, adaptable, and extensible manner.  相似文献
9.
We formalize natural deduction for first-order logic in the proof assistant Coq, using de Bruijn indices for variable binding. The main judgment we model is of the form d[:], stating that d is a proof term of formula under hypotheses it can be viewed as a typing relation by the Curry–Howard isomorphism. This relation is proved sound with respect to Coq's native logic and is amenable to the manipulation of formulas and of derivations. As an illustration, we define a reduction relation on proof terms with permutative conversions and prove the property of subject reduction.  相似文献
10.
We present a formal proof (at the implementation level) of an efficient algorithm proposed by P. Zimmermann in 1999 to compute square roots of arbitrarily large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library, is completely proven within the COQ system. Proofs are developed using the CORRECTNESS tool to deal with imperative features of the program. The formalization is rather large (more than 13,000 lines) and requires some advanced techniques for proof management and reuse.  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号