A Fuzzy Proof Theory

Based on the first order peicate logic,in this paper,we present a new approach to generalizing the syntax of ordinary Horn clause rules to establish a fuzzy proof theory,First of all,each Horn clause rule is associated with a numerical implication strength f.Therefore we obtain f-Horn clause rules.Secondly,Herbrand interpretations can be generalized to fuzzy subsets of the Herbrand base in the sense of Zadch.As a result the proof theory for Horn clause rules can be developed in much the same way for f-Horm clause rules.     

Proof Pearl: Mechanizing the Textbook Proof of Huffman’s Algorithm

Huffman’s algorithm is a procedure for constructing a binary tree with minimum weighted path length. Our Isabelle/HOL proof closely follows the sketches found in standard algorithms textbooks, uncovering a few snags in the process. Another distinguishing feature of our formalization is the use of custom induction rules to help Isabelle’s automatic tactics, leading to very short proofs for most of the lemmas. This work was supported by the DFG grant NI 491/11-1.     

弹速工具——Bullet Proof FTP

Ｂｕｌｌｅｔ Ｐｒｏｏｆ ＦＴＰ,正如其名是一款超速 ＦＴＰ软件,其强大的功能与ＣｕｔｅＦＴＰ和ＷＳ－ＦＴＰ相比是有过之而不及的。其界面友好,摆脱了传统ＦＴＰ软件古板、单纯菜单操作的格调,使用了更多更鲜明的按钮,提供了强大的按钮自编辑功能。相信老网友们一定会踢掉ＣｕｔｅＦＴＰ,改用更小更优秀的 Ｂｕｌｌｅｔ ＰｒｏｏｆＦＴＰ。一、下载与安装 首先,您可以到ｌｉｂ．ｗｕｈｅｅ．ｅｅｄｕ．ｃｎ／ｐｕｂ／ｉｎｔｅｒｎｅｔ／ｆｔｐ／ｂｐｆｔｐ１１５ｃ．ｚｉｐ下载该软件,大小为６３５Ｋｂ,安装也非常简单,按部就…     

FTP的利器——Bullet Proof FTP

随着Internet的逐步普及,网民们对各类软件的需求量也不断增加,网上众多的FIP(File Transfer Protocol,文件传输协议)站点更成丁我们实现资源共享、获取软件的好地方。如何将众多好软件“据为己有”?面对各种FIP软件又如何选择?这些都是刚接     

A Proof Rule for While Loop in VDM

A proof rule for while loop which can be used in justification of programs w.r.t.specifications using two-state post-conditions is presented in this paper,accompanied with a soundness proof and a comparison with Aczel‘w rule for while loop     

Proof movie — A proof with the Boyer-Moore prover

This paper uses the Boyer-Moore prover for developing a proof of correctness for the implementation of a very small compiler. The polished version of the proof is included as an appendix. The major intent of the paper is to describe the process of proving using an automatic theorem prover.This paper presents work done when the author was employed at the University of Kiel, Germany. The research was partially funded by the Commission of the European Communities (CEC) under the ESPRIT programme in the field of Basic Research Action proj. no. 3104, ProCoS: Provably Correct Systems     

Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Avoiding deadlock is crucial to interconnection networks. In ’87, Dally and Seitz proposed a necessary and sufficient condition for deadlock-free routing. This condition states that a routing function is deadlock-free if and only if its channel dependency graph is acyclic. We formally define and prove a slightly different condition from which the original condition of Dally and Seitz can be derived. Dally and Seitz prove that a deadlock situation induces cyclic dependencies by reductio ad absurdum. In contrast we introduce the notion of a waiting graph from which we explicitly construct a cyclic dependency from a deadlock situation. Moreover, our proof is structured in such a way that it only depends on a small set of proof obligations associated to arbitrary routing functions and switching policies. Discharging these proof obligations is sufficient to instantiate our condition for deadlock-free routing on particular networks. Our condition and its proof have been formalized using the ACL2 theorem proving system.     

An Algebraic Characterization of Inductive Soundness in Proof by Consistency

Kapur and Musser studied the theoretical basis for proof by consistency and obtained an inductive completeness result:p=q if and only if p=q is true in every inductive model.However,there is a loophole in their proof for the soundness part:p=q implies p=q is true in every inductive model.The aim of this paper is to give a correct characterization of inductive soundness from an algebraic view by introducing strong inductive models.     

A Semantic Proof of Polytime Soundness of Light Affine Logic

We define realizability semantics for Light Affine Logic ( LAL\mathsf{LAL} ) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-soundness of LAL\mathsf{LAL} which is considerably simpler than the standard proof based on proof nets and is entirely semantical in nature. The model construction uses a new instance of a resource monoid; a general method for interpreting systems based on Linear Logic introduced earlier by the authors.     

按劳分配按需所取——Radware智能链路负载均衡产品Link Proof

全球智能应用交换机领导者与应用安全技术挑战者Radware公司．针对企业总部推出的多链路应用访问链路均衡产品Link Proof,为企业总部提供了完整的应用访问解决方案。通过Link Proof，使企业能够在广域网范围内的任何地方实现连续的远程用户访问和最佳的分布式应用交付。同时，Link Proof强化了企业多链路连接管理、广域网加速应用和应用安全，以提供全面完善的功能，从而为数据中心的所有关键性业务提供可靠的Internet连接和快速响应时间。     

A Syntactic Proof of the Conservativity ofλ_ω overλ_2

In this paper,the relationship between the second order typed λ－calculus λ2 and its higher order version λω is discussed.A purely syntactic proof of the conservativity of λωover λ2 is given.     

A Simple Proof of the Jamiołkowski Criterion for Complete Positivity of Linear Maps

We give a simple direct proof of the Jamiołkowski criterion to check whether a linear map between matrix algebras is completely positive or not. This proof is more accessible for physicists than other ones found in the literature and provides a systematic method to give any set of Kraus matrices of the Kraus decomposition.Presented at the 36th Symposium on Mathematical Physics, “Open Systems & Quantum Information”, Toruń, Poland, June 9-12, 2004.     

The <Emphasis Type="Italic">λ</Emphasis>-Calculus and the Unity of Structural Proof Theory

In the context of intuitionistic implicational logic, we achieve a perfect correspondence (technically an isomorphism) between sequent calculus and natural deduction, based on perfect correspondences between left-introduction and elimination, cut and substitution, and cut-elimination and normalisation. This requires an enlarged system of natural deduction that refines von Plato’s calculus. It is a calculus with modus ponens and primitive substitution; it is also a “coercion calculus”, in the sense of Cervesato and Pfenning. Both sequent calculus and natural deduction are presented as typing systems for appropriate extensions of the λ-calculus. The whole difference between the two calculi is reduced to the associativity of applicative terms (sequent calculus = right associative, natural deduction = left associative), and in fact the achieved isomorphism may be described as the mere inversion of that associativity. The novel natural deduction system is a “multiary” calculus, because “applicative terms” may exhibit a list of several arguments. But the combination of “multiarity” and left-associativity seems simply wrong, leading necessarily to non-local reduction rules (reason: normalisation, like cut-elimination, acts at the head of applicative terms, but natural deduction focuses at the tail of such terms). A solution is to extend natural deduction even further to a calculus that unifies sequent calculus and natural deduction, based on the unification of cut and substitution. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions.     

Towards Proof Planning for ω

This paper describes the proof planning system _ω⁺ for the meta theorem prover for LF implemented in Twelf. The main contributions include a formal system that approximates the flow of information between assumptions and goals within a meta proof, a set of inference rules to reason about those approximations, and a soundness proof that guarantees that the proof planner does not reject promising proof states. Proof planning in _ω⁺ is decidable.     

On the Comparison of Proof Planning Systems: , Ωmega and IsaPlanner

We present a framework for describing proof planners. This framework is based around a decomposition of proof planners into planning states, proof language, proof plans, proof methods, proof revision, proof control and planning algorithms.We use this framework to motivate the comparison of three recent proof planning systems, λCLaM, Ωmega and IsaPlanner, and demonstrate how the framework allows us to discuss and illustrate both their similarities and differences in a consistent fashion. This analysis reveals that proof control and the use of contextual information in planning states are key areas in need of further investigation.