活塞式标准体积管发展现状

标准体积管是一种常见的检定液体流量计的流量标准装置,其结构简单、使用方便、应用广泛,特别适合现场校准,但目前仍缺乏对体积管发展现状进行系统梳理的研究。针对此问题做了深入的文献调研,主要研究内容为：回顾国内外标准体积管的发展历程;简述标准体积管的基本原理和应用场景;对比分析不同类型体积管的性能特点;归纳了体积管的未来发展方向,为下一代体积管技术研发提供参考。     

Formal reasoning in intelligent database systems

Expert database systems were proposed to solve the difficulties encountered in traditional database systems. Prolog provides a fast prototyping tool for building such database systems. However, an intelligent database system implemented in Prolog faces a major restriction that only Horn rules are allowed in the knowledge base. We propose a theorem prover which can make inference for non-Horn intelligent database systems. Conclusions can be deduced from the facts and rules stored in a knowledge base. For a knowledge base with a finite domain, the prover can provide correct answers to queries, derive logical consequences of the database, and provide help in detecting inconsistencies or locating bugs in the database. The theorem prover is efficient in deriving conclusions from large knowledge bases which might swamp most of the other deductive systems. The theorem prover is also useful in solving heuristically the satisfiability problem related to a database with an infinite domain. A truth maintenance mechanism is provided to help eliminate repetitious work for the same goals.Supported by National Science Council under grant NSC 81-0408-E-110-9.     

ACT-P: A configurable theorem-prover

There has been a considerable amount of research into the provision of explicit representation of control regimes for resolution-based theorem provers. However, most of the existing systems are either not adequate or too inefficient to be of practical use. In this paper a theorem prover, ACT-P, which is adequate but retains satisfactory efficiency is presented. It does so by providing a number of user-changeable heuristics which are called at specific points during the search for a proof. The set of user-changeable heuristics was determined on the basis of a classification of the heuristics used by existing resolution-based theorem provers.     

A mechanical proof of Segall's PIF algorithm

We describe the construction of a distributed algorithm with asynchronous communication together with a mechanically verified proof of correctness. For this purpose we treat Segall's PIF algorithm (propagation of information with feedback). The proofs are based on invariants, and variant functions for termination. The theorem prover NQTHM is used to deal with the many case distinctions due to asynchronous distributed computation. Emphasis is on the modelling assumptions, the treatment of nondeterminacy, the forms of termination detection, and the proof obligations for a complete mechanical proof. Finally, a comparison is made with (the proof of) the minimum spanning tree algorithm of Gallager, Humblet, and Spira, for which the technique was developed.     

Computer proofs in Group Theory

This paper reports the results of an experiment in using the Boyer-Moore Theorem Prover in seeking computer-checked proofs in Group Theory. Starting from the axioms for groups and elementary list and number theory, the theorem prover was led to the proofs of two basic theorems in Elementary Group Theory by a sequence of lemmas suggested by the author. The computer proofs illustrate the effective use of the Boyer-Moore Theorem Prover in Group Theory.     

An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem

This paper describes the use of the Boyer-Moore theorem prover in mechanically generating a proof of Wilson's theorem: for any prime p, (p-1)! and p-1 are congruent modulo p. The input to the theorem prover consists of a sequence of three function definitions and forty-two propositions to be proved. The proofs generated by the system are based on a library of lemmas relating to list manipulation and number theory, including Fermat's theorem.     

Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL

Real-time systems usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism, which makes their performance analysis quite complex. Thus, traditional techniques, such as simulation, or the state-based formal methods usually fail to produce reasonable results. In this paper, we propose to use higher-order-logic (HOL) theorem proving for the performance analysis of real-time systems. The idea is to formalize the real-time system as a logical conjunction of HOL predicates, whereas each one of these predicates define an autonomous component or process of the given real-time system. The random or unpredictable behavior found in these components is modeled as random variables. This formal specification can then be used in a HOL theorem prover to reason about both functional and performance related properties of the given real-time system. In order to illustrate the practical effectiveness of our approach, we present the analysis of the Stop-and-Wait protocol, which is a classical example of real-time systems. The functional correctness of the protocol is verified by proving that the protocol ensures reliable data transfers. Whereas, the average message delay relation is verified in HOL for the sake of performance analysis. The paper includes the protocol’s formalization details along with the HOL proof sketches for the major theorems.     

用于指针逻辑的自动定理证明器

提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL 的工具中得以实现.APL 自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.     

A family of goal directed theorem provers based on conjunction and implication: Part 1

This paper presents a family of theorem provers for classical, intuitionistic and neighbouring logics. The theorem provers are based on a formulation of these logics in terms of conjunction, implication and falsity. Computation is goal directed, and, for the special case of Horn clauses, coincides with pure Prolog computation. Our approach is generic, and, as we shall show in a subsequent paper, can be adapted to other logics, such as modal and temporal systems.The research described in this paper has been funded partially by Esprit project No. 393, ACORD, of the European Commission.     

A mechanical proof of Quadratic Reciprocity

We describe the use of the Boyer-Moore theorem prover in mechanically generating a proof of the Law of Quadratic Reciprocity: for distinct odd primes p and q, the congruences x ² q (mod p) and x ² p (mod q) are either both solvable or both unsolvable, unless pq3 (mod 4). The proof is a formalization of an argument due to Eisenstein, based on a lemma of Gauss. The input to the theorem prover consists of nine function definitions, thirty conjectures, and various hints for proving them. The proofs are derived from a library of lemmas that includes Fermat's Theorem and the Gauss Lemma.