The axiomatic semantics of programs based on Hoare's logic

Summary This paper is about the Floyd-Hoare Principle which says that the semantics of a programming language can be formally specified by axioms and rules of inference for proving the correctness of programs written in the language. We study the simple language WP of while-programs and Hoare's system for partial correctness and we calculate the relational semantics of WP as this is determined by Hoare's logic. This calculation is possible by using relational semantics to build a completeness theorem for the logic. The resulting semantics AX we call the axiomatic relational semantics for WP. This AX is not the conventional semantics for WP: it need not be effectively computable or deterministic, for example. A large number of elegant properties of AX are proved and the Floyd-Hoare Principle is reconsidered.     

Theorem Proving Modulo

Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate computations and deductions in a clean way. The first contribution of this paper is to define a sequent calculus modulo that gives a proof-theoretic account of the combination of computations and deductions. The congruence on propositions is handled through rewrite rules and equational axioms. Rewrite rules apply to terms but also directly to atomic propositions. The second contribution is to give a complete proof search method, called extended narrowing and resolution (ENAR), for theorem proving modulo such congruences. The completeness of this method is proved with respect to provability in sequent calculus modulo. An important application is that higher-order logic can be presented as a theory in deduction modulo. Applying the ENAR method to this presentation of higher-order logic subsumes full higher-order resolution. This revised version was published online in August 2006 with corrections to the Cover Date.     

On the calculus of positively constructed formulas for automated theorem proving

The paper deals with an expressive logic language LF and its calculus. Formulas of this language consist of some large-scale structural elements, such as type quantifiers. The language LF contains only two logic symbols—∀ and ∃, which form the set of logic connectives of the language. The logic calculus JF and complete strategy for automated proof search based on a single unary rule of inference are considered. This calculus has a number of other features which lead to the reduction of the combinatorial complexity of finding the deductions in comparison to the known systems for automated theorem proving as the Resolution method and Genzen calculus. Problems of effective implementation of JF as a program system for automated theorem proving are considered.     

Knowledge Representation of Software Component Interconnection Information for Large-Scale Software Modifications

Logic can be used to precisely express human thoughts and inferences. In this paper, an approach using first-order logic for knowledge representation of software component interconnection information to facilitate the validity and integrity checking of the interconnection among software components during software development or modification is presented. Directed graphs are first used to model the structure and behavior of a large-scale software system, and a first-order theory of directed graphs (the DG theory) is established. The interconnection behavior among software components in a large-scale software system is a directed graph which is called software component interconnection graph (CIG). The behavior of the CIG is interpreted using the DG theory and translated into logic representation. The translated logic representation is a set of logic clauses and can be considered as a set of axioms. Automated reasoning techniques based on these axioms can be used to perform the validity and integrity checking of software properties in the software development or maintenance phase.     

支持索引式的PPTL定理证明器的实现

定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.     

A pragmatic approach to resolution-based theorem proving

Resolution theory offers a simple, complete method for proving theorems but is generally considered impractical. The theorems we are interested in proving arise in the analysis of programs and usually involve quantification. We have developed a system for proving these theorems using resolution, but have embedded in it a simplifier as the central component. The simplifier is an integrated collection of algorithms for normalizing arithmetic, relational, and logical expressions. The knowledge in the simplifier is encoded in procedures, rather than as axioms or rules. We use the simplifier to prove certain theorems, reduce the clutter in theorems, and reduce the cost of unification, Inherent in the normal form algorithms is the notion of strengthening (e.g., inferringa =b froma b ANDb a). We have incorporated the notion into the unification algorithm as well. The design of the system permits its use along a spectrum from pure resolution to resolution with interpretation of the arithmetic and relational operators. Strengthening is a heuristic that permits the movement along this spectrum. We call the approachi-resolution.i-resolution does not preserve completeness; it does define a means for approaching completeness efficiently and systematically. It thus attempts to provide a pragmatic approach to mechanical theorem proving.     

Specification and synthesis of hybrid automata for physics-based animation

Physics-based animation programs can often be modeled in terms of hybrid automata. A hybrid automaton includes both discrete and continuous dynamical variables. The discrete variables define the automaton’s modes of behavior. The continuous variables are governed by mode-dependent differential equations. This paper describes a system for specifying and automatically synthesizing physics-based animation programs based on hybrid automata. The system presents a program developer with a family of parameterized specification schemata. Each schema describes a pattern of behavior as a hybrid automaton passes through a sequence of modes. The developer specifies a program by selecting one or more schemata and supplying application-specific instantiation parameters for each of them. Each schema is associated with a set of axioms in a logic of hybrid automata. The axioms serve to document the semantics of the specification schema. Each schema is also associated with a set of implementation rules. The rules synthesize program components implementing the specification in a general physics-based animation architecture. The system allows animation programs to be developed and tested in an incremental manner. The system itself can be extended to incorporate additional schemata for specifying new patterns of behavior, along with new sets of axioms and implementation rules. It has been implemented and tested on over a dozen examples. We believe this research is a significant step toward a specification and synthesis system that is flexible enough to handle a wide variety of animation programs, yet restricted enough to permit programs to be synthesized automatically.     

Resolution theorem proving in reified modal logics

This paper is concerned with the application of the resolution theorem proving method to reified logics. The logical systems treated include the branching temporal logics and logics of belief based on K and its extensions. Two important problems concerning the application of the resolution rule to reified systems are identified. The first is the redundancy in the representation of truth functional relationships and the second is the axiomatic reasoning about modal structure. Both cause an unnecessary expansion in the search space. We present solutions to both problems which allow the axioms defining the reified logic to be eliminated from the database during theorem proving hence reducing the search space while retaining completeness. We describe three theorem proving methods which embody our solutions and support our analysis with empirical results.Much of the research reported in this paper was supported by DTI IED SERC grant No. GR/F 35968, and was carried out whilst Han Reichgelt was at the University of Nottingham.     

Mothers of Pipelines

We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set architecture (ISA). The MOP vs. ISA correctness theorem splits naturally into a large number of simple subgoals. This theorem reduces proving the correctness of a given pipelined implementation of the ISA to verifying that each of its transitions can be modeled as a sequence of MOP state transitions.     

Automated Procedure Construction for Deductive Synthesis

Deductive program synthesis systems based on automated theorem proving offer the promise of software that is correct by construction. However, the difficulty encountered in constructing usable deductive synthesis systems has prevented their widespread use. Amphion is a real-world, domain-independent, completely automated program synthesis system. It is specialized to specific applications through the creation of an operational domain theory and a specialized deductive engine. This paper describes an experiment aimed at making the construction of usable Amphion applications easier.The software system Theory Operationalization for Program Synthesis (TOPS) has a library of decision procedure templates with a theory schema for each procedure. TOPS identifies sets of axioms in the domain theory that are instances of theory schema associated with library procedures. For each procedure instance, TOPS uses iterated partial deduction to augment the procedure with the capability to construct ground terms for deductive synthesis. Synthesized procedures are interfaced to a resolution theorem prover. Axioms in the original domain theory that are implied by the synthesized procedures are removed.The inference rules of the theorem prover have been extended so that during deductive synthesis, each procedure is invoked to test conjunctions of literals in the language of the theory of that procedure. When possible, the procedure generates ground terms and binds them to variables in a problem specification. These terms are program fragments. Experiments show that the procedures synthesized by TOPS can reduce theorem proving search at least as much as hand tuning of the deductive synthesis system.     

Internal axioms for domain semirings

New axioms for domain operations on semirings and Kleene algebras are proposed. They generalise the relational notion of domain-the set of all states that are related to some other state-to a wide range of models. They are internal since the algebras of state spaces are induced by the domain axioms. They are simpler and conceptually more appealing than previous two-sorted external approaches in which the domain algebra is determined through typing. They lead to a simple and natural algebraic approach to modal logics based on equational reasoning. The axiomatisations have been developed in a new style of computer-enhanced mathematics by automated theorem proving, and the approach itself is suitable for automated systems analysis and verification. This is demonstrated by a fully automated proof of a modal correspondence result for Löb’s formula that has applications in termination analysis.     

Decision Planning Knowledge Representation Framework: A Case-Study

This paper discusses experiences and perspectives of utilisation of declarative knowledge structures as a convenient knowledge base medium in configuration expert systems. Although many successful systems have been developed, these are often difficult to maintain and to generalize in rapidly changing domains. In this paper we address the problem of building intelligent knowledge based systems with emphasis on their maintainability. Firstly, several industrial applications of proof planning, a theorem proving technique, will be described and their advantages and flaws will be discussed. This discussion is followed by the theoretical foundation of decision planning knowledge representation framework that, based on proof planning, facilitates separate administration of inference problem solving knowledge and the domain theory axioms. Machine learning methods for maintaining the inference knowledge to be up-to-date with permanently changing domain theory are commented and evaluated.     

Extending a brainiac prover to lambda-free higher-order logic

Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to \(\lambda \)-free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

     

Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis

This paper presents a formal specification and a proof of correctness for the widely-used Force-Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling of data flow graphs in high-level synthesis systems. The proof effort is conducted using a higher-order logic theorem prover. During the proof effort many interesting properties of the FDLS algorithm are discovered. These properties are formally stated and proved in a higher-order logic theorem proving environment. These properties constitute a detailed set of formal assertions and invariants that should hold at various steps in the FDLS algorithm. They are then inserted as programming assertions in the implementation of the FDLS algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the FDLS algorithm produced correct schedules and, (2) in the event of failure, help discover and isolate programming errors in the FDLS implementation.We present a detailed example and several experiments to demonstrate the effectiveness of these assertions in discovering and isolating errors. Based on this experience, we discuss the role of the formal theorem proving exercise in developing a useful set of assertions for embedding in the scheduler code and argue that in the absence of such a formal proof checking effort, discovering such a useful set of assertions would have been an arduous if not impossible task.     

Completeness and Counter-Example Generations of a Basic Protocol Logic: (Extended Abstract)

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a “trace” any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.     

An experimental logic based on the fundamental deduction principle

Experimental logic can be viewed as a branch of logic dealing with the actual construction of useful deductive systems and their application to various scientific disciplines. In this paper we describe an experimental deductive system called the SYMbolic EVALuator (i.e. SYMEVAL) which is based on a rather simple, yet startling principle about deduction, namely that deduction is fundamentally a process of replacing expressions by logically equivalent expressions. This principle applies both to logical and domain-dependent axioms and rules. Unlike more well-known logical inference systems which do not satisfy this principle, herein is described a system of logical axioms and rules called the SYMMETRIC LOGIC which is based on this principle. Evidence for this principle is given by proving theorems and performing deduction in the areas of set theory, logic programming, natural language analysis, program verification, automatic complexity analysis, and inductive reasoning.     

Nominal logic, a first order theory of names and binding

This paper formalises within first-order logic some common practices in computer science to do with representing and reasoning about syntactical structures involving lexically scoped binding constructs. It introduces Nominal Logic, a version of first-order many-sorted logic with equality containing primitives for renaming via name-swapping, for freshness of names, and for name-binding. Its axioms express properties of these constructs satisfied by the FM-sets model of syntax involving binding, which was recently introduced by the author and M.J. Gabbay and makes use of the Fraenkel–Mostowski permutation model of set theory. Nominal Logic serves as a vehicle for making two general points. First, name-swapping has much nicer logical properties than more general, non-bijective forms of renaming while at the same time providing a sufficient foundation for a theory of structural induction/recursion for syntax modulo α-equivalence. Secondly, it is useful for the practice of operational semantics to make explicit the equivariance property of assertions about syntax – namely that their validity is invariant under name-swapping.     

Conceptual modeling of data base operations

A formalism adequate for the specification of behavioral properties of data bases is proposed. The formalism is a many-sorted first order predicate calculus, including a formalized notion of data base state. Both update and query requests are modeled through expressions by the use of predicates supplied in the language of the formal system, and are treated uniformly as a theorem proving process. The process consists of using the axioms defining the data base for either synthesizing a valid sequence of update operations (if such exists) or for answering the query.     

基于目标演绎距离的一阶逻辑子句集预处理方法

一阶逻辑定理证明是人工智能的核心基础,研究一阶逻辑自动定理证明器的相关理论和高效的算法实现具有重要的学术意义。当前一阶逻辑自动定理证明器首先通过子句集预处理约简子句集规模,然后通过演绎方法对定理进行判定。现有的应用于证明器中的子句集预处理方法普遍只从与目标子句项符号相关性角度出发,不能很好地从文字的互补对关系中体现子句间的演绎。为了在子句集预处理时从演绎的角度刻画子句间的关系,定义了目标演绎距离的概念并给出了计算方法,提出了一种基于目标演绎距离的一阶逻辑子句集预处理方法。首先对原始子句集进行包含冗余子句约简并应用纯文字删除规则,然后根据目标子句计算剩余子句集中的文字目标演绎距离、子句目标演绎距离,并最终通过设定子句演绎距离阈值来实现对子句集的进一步预处理。将该预处理方法应用于顶尖证明器Vampire,以2017年国际一阶逻辑自动定理证明器标准一阶逻辑问题组竞赛例为测试对象,在标准的300 s内,加入提出的子句集预处理方法的Vampire4.1相比原始的Vampire4.1多证明4个定理,能证明10个Vampire4.1未证明的定理,占其未证明定理总数的13.5%;在证明的定理中,提出的...