Proof by analogy in mural

An important advantage of using a formal method of developing software is that one can prove that development steps are correct with respect to their specification. Conducting proofs by hand, however, can be time consuming to the extent that designers have to judge whether a proof of a particular obligation is worth conducting. Even if hand proofs are worth conducting, how do we know that they are correct? One approach to overcoming this problem is to use an automatic theorem proving system to develop and check our proofs. However, in order to enable present day theorem provers to check proofs, one has to conduct them in much more detail than hand proofs. Carrying out more detailed proofs is of course more time consuming. This paper describes the use of proof by analogy in an attempt to reduce the time spent on proofs. We develop and implement a proof follower based on analogy and present an example to illustrate its characteristics. The example shows that even when the follower fails to complete a proof, it can provide a hint that enables the user to complete a proof.     

Proving Invariants of I/O Automata with TAME

This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify and prove properties of an I/O automaton efficiently and without first becoming a PVS expert. To accomplish this goal, TAME provides a template that the user completes to specify an I/O automaton and a set of proof steps natural for humans to use for proving properties of automata. Each proof step is implemented by a PVS strategy and possibly some auxiliary theories that support that strategy. We have used the results of two recent formal methods studies as a basis for two case studies to evaluate TAME. In the first formal methods study, Romijn used I/O automata to specify and verify memory and remote procedure call components of a concurrent system. In the second formal methods study, Devillers et al. specified a tree identify protocol (TIP), part of the IEEE 1394 bus protocol, and provided hand proofs of TIP properties. Devillers also used PVS to specify TIP and to check proofs of TIP properties. In our first case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata formulated by Romijn and Devillers et al. and to check their hand proofs. In our second case study, the TAME approach to verification was compared with an alternate approach by Devillers which uses PVS directly.     

Using induction and rewriting to verify and complete parameterized specifications

In software engineering there is a growing demand for formal methods for the specification and validation of software systems. The formal development of a system might give rise to many proof obligations. We must prove the completeness of the specification and the validity of some inductive properties. In this framework, many provers have been developed. However they require much user interaction even for simple proof tasks. In this paper, we present new procedures to test sufficient completeness and to prove or disprove inductive properties automatically in para-meterized conditional specifications. The method has been implemented in the prover SPIKE. Computer experiments illustrate the improvements in length and structure of proofs, due to parameterization. Moreover, SPIKE offers facilities to check and complete specifications.     

A framework for counterexample generation and exploration

Model-checking is becoming an accepted technique for debugging hardware and software systems. Debugging is based on the “Check/Analyze/Fix” loop: check the system against a desired property, producing a counterexample when the property fails to hold; analyze the generated counterexample to locate the source of the error; fix the flawed artifact—the property or the model. The success of model-checking non-trivial systems critically depends on making this Check/Analyze/Fix loop as tight as possible. In this paper, we concentrate on the Analyze part of the debugging loop. To this end, we present a framework for generating, structuring and exploring counterexamples, implemented in a tool called KEGVis. The framework is based on the idea that the most general type of evidence to why a property holds or fails to hold is a proof. Such proofs can be presented to the user in the form of proof-like counterexamples, without sacrificing any of the intuitiveness and close relation to the model that users have learned to expect from model-checkers. Moreover, proof generation is flexible, and can be controlled by strategies, whether built into the tool or specified by the user, thus enabling generation of the most “interesting” counterexample and its interactive exploration. Moreover, proofs can be used to generate and display all relevant evidence together, a technique referred to as abstract counterexamples. Overall, our framework can be used for explaining the reason why the property failed or succeeded, determining whether the property was correct (“specification debugging”), and for general model exploration.     

基于用户自添加规则的自动推理程序

基于前推搜索算法的自动推理软件近年来相继出现,该类软件利用几何定理可读证明的特性,和用户进行交互解题.但这类软件都是将推理的规则作为内置函数处理,用户只能选择软件提供的规则进行推理.设计了用户可添加规则的算法,即用户可以将自己的知识作为规则添加到软件中来进行推理.该算法已被编制成程序.     

Automated production of traditional proofs for theorems in Euclidean geometry I. The Hilbert intersection point theorems

We present a method which can produce traditional proofs for a class of constructive geometry statements in Euclidean geometry. The method is a mechanization of the traditional area method used by many geometers. The key idea of our method is to eliminate dependent (constructed) points in a geometry statement using a few basic geometry propositions about the area of triangles. The method has been implemented. Our program, calledEuclid, can produce traditional proofs of many hard geometry theorems such as Pappus' theorem, Pascal's theorem, Gauss point theorem, and the Pascal conic theorem. Currently, it has produced proofs of 110 nontrivial theoremsentirely automatically. The proofs produced byEuclid are elegant, short (often shorter than the proofs given by geometers) and understandable even to high school students. This method seems to be the first that can produce traditional proofs for hard geometry theorems automatically.The work reported here was supported in part by the NSF Grant CCR-9117870 and the Chinese National Science Foundation.On leave from the Institute of Systems Sciences, Academia Sinica, Beijing 100080, P.R. China.     

A framework for checking proofs naturally

We propose a logical framework, called Natural Framework (NF), which supports formal reasoning about computation and logic (CAL) on a computer. NF is based on a theory of Judgments and Derivations. NF is designed by observing how working mathematical theories are created and developed. Our observation is that the notions of judgments and derivations are the two fundamental notions used in any mathematical activity. We have therefore developed a theory of judgments and derivations and designed a framework in which the theory provides a uniform and common play ground on which various mathematical theories can be defined as derivation games and can be played, namely, can write and check proofs. NF is equipped with a higher-order intuitionistic logic and derivations (proofs) are described following Gentzen’s natural deduction style. NF is part of an interactive computer environment CAL and it is also referred to as NF/CAL. CAL is written in Emacs Lisp and it is run within a special buffer of the Emacs editor. CAL consists of user interface, a general purpose parser and a checker for checking proofs of NF derivation games. NF/CAL system has been successfully used as an education system for teaching CAL for undergraduate students for about 8 years. We will give an overview of the NF/CAL system both from theoretical and practical sides.     

On the desirability of mechanizing calculational proofs

Dijkstra argues that calculational proofs are preferable to traditional pictorial and/or verbal proofs. First, due to the calculational proof format, incorrect proofs are less likely. Second, syntactic considerations (letting the “symbols do the work”) have led to an impressive array of techniques for elegant proof construction. However, calculational proofs are not formal and are not flawless. Why not make them formal and check them mechanically?     

The RISC ProofNavigator: a proving assistant for program verification in the classroom

This paper gives an overview of the RISC ProofNavigator, an interactive proving assistant for the area of program verification. The assistant combines the user-guided top-down decomposition of proofs with the automatic simplification and closing of proof states by an external satisfiability solver. The software exhibits a modern graphical user interface which has been developed with a focus on simplicity in order to make the software suitable for educational scenarios. Nevertheless, some use cases of a certain level of complexity demonstrate that it may be also appropriate for various realistic applications. D. A. Duce, J. Oliveira, P. Boca and R. Boute     

Reduced GUI for an interactive geometry software: Does it affect students' performance?

PurposeThe purpose of this paper is to describe an experimental study to reduce cognitive load and enhance usability for interactive geometry software.Design/methodology/approachThe Graphical User Interface is the main mechanism of communication between user and system features. Educational software interfaces should provide useful features to assist learners without generate extra cognitive load. In this context, this research aims at analyzing a reduced and a complete interface of interactive geometry software, and verifies the educational benefits they provide. We investigated whether a reduced interface makes few cognitive demands of users in comparison to a complete interface. To this end, we designed the interfaces and carried out an experiment involving 69 undergraduate students.FindingsThe experimental results indicate that an interface that hides advanced and extraneous features helps novice users to perform slightly better than novice users using a complete interface. After receiving proper training, however, a complete interface makes users more productive than a reduced interface.Originality/valueIn educational software, successful user interface designs minimize the cognitive load on users; thereby users can direct their efforts to maximizing their understanding of the educational concepts being presented.     

Finding Proofs in Tarskian Geometry

We report on a project to use a theorem prover to find proofs of the theorems in Tarskian geometry. These theorems start with fundamental properties of betweenness, proceed through the derivations of several famous theorems due to Gupta and end with the derivation from Tarski’s axioms of Hilbert’s 1899 axioms for geometry. They include the four challenge problems left unsolved by Quaife, who two decades ago found some OTTER proofs in Tarskian geometry (solving challenges issued in Wos’s 1998 book). There are 212 theorems in this collection. We were able to find OTTER proofs of all these theorems. We developed a methodology for the automated preparation and checking of the input files for those theorems, to ensure that no human error has corrupted the formal development of an entire theory as embodied in two hundred input files and proofs. We distinguish between proofs that were found completely mechanically (without reference to the steps of a book proof) and proofs that were constructed by some technique that involved a human knowing the steps of a book proof. Proofs of length 40–100, roughly speaking, are difficult exercises for a human, and proofs of 100–250 steps belong in a Ph.D. thesis or publication. 29 of the proofs in our collection are longer than 40 steps, and ten are longer than 90 steps. We were able to derive completely mechanically all but 26 of the 183 theorems that have “short” proofs (40 or fewer deduction steps). We found proofs of the rest, as well as the 29 “hard” theorems, using a method that requires consulting the book proof at the outset. Our “subformula strategy” enabled us to prove four of the 29 hard theorems completely mechanically. These are Ph.D. level proofs, of length up to 108.     

基于消点法的几何自动推理系统实现

为了实现几何自动推理的可读性证明,并提高推理效率,介绍了一个基于消点法的可构造性几何命题自动推理系统的设计与实现。该系统提供作图的方式接受用户的几何命题前提条件的输入,可以对初等几何中的大部分可构造性几何问题进行自动证明和求解,并生成可读的证明步骤,大大方便了初高等几何教育和相关研究者的需要。     

Windows环境下塔板设计软件的开发

现有的塔板设计软件一般是在ＤＯＳ或ＵＮＩＸ操作系统下运行的，使用上有不少缺陷，针对塔板设计过程的特点，我们以Ｗｉｎｄｏｗｓ作为操作系统，以功能很强的ＶｉｓｎａｌＢａｓｉｃ作为开发工具，开发了一个新的塔板设计软件ＴＣＤ，与其他塔板设计软件相比，ＴＣＤ具有良好的用户界面，人机对话功能和图形功能，易学易用，用ＴＣＤ既可以进行新塔设计，也可以对旧塔进行校核和改造设计，具有良好的实用价值。     

几何定理可读证明的自动生成

用计算机能生成几何定理的易为人们理解的证明吗？这个几十年来进展很小的难题,自１９９２年以来有了突破性进展,对于一大类欧几何命题－构造几何例题,已有了相当有效的算法,基于此算法所编制的程序,已证明了５００多非平凡的几何例题,对其中大多数例题,机器自动生的证明是简明而易于理解的,本文是对这一领域近三年来取得的进展的综述,包括了在非欧几何可读证明方面的最新成果。     

Validation of HOL Proofs by Proof Checking

Formal proofs generated by mechanised theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an implementation of a proof checker which is able to check a practical proof consisting of thousands of inference steps.     

中学几何学习软件的设计与实现

以中学几何证明题为例，介绍了一个运用计算机帮助学生在 解题过程中自动查错的软件设计方法，系统克服了以往的CAI软件不能检查学生解题过程的 正误及只能让学生做题库中的题的缺点，还可将其改为倒推法，实现自动解题的设想。     

基于Web的企业仓储管理系统的研究与实现

基于Web的企业仓储管理系统的研究与实现是针对企业仓库材料的出入库登记和查询统计等方面而开发的管理软件,是一款适用于中小企业的先进的管理信息系统。该系统针对企业需要,以入库管理和出库管理为重点,实现仓储材料的出入库管理、查询管理及用户管理等功能。     

Development of an Intelligent Wheelchair Using Computer Graphics Animation and Simulation

A new robot simulator JC-1 is used as a control software development tool in a project in progress where an intelligent wheelchair for a blind user is being developed. The intelligent wheelchair is planned to be able to fulfill simple symbolic commands like "follow wall" or "follow object" and using the JC-1 simulator an evaluation team which includes e.g. the user, a rehabilitation engineer and a software engineer, can check control algorithms and user interface routines before constructing a real wheelchair prototype. The JC-1 simulator models the environment using simplified boundary- representation where objects, robot sensors and actuators are presented as symbolic objects in the graphics data-base of the simulator. In the JC-1 simulator a robot controller under development controls the motion of the graphical model of the robot while simulator commands or other robot controllers can be used to control the movement of disturbing obstacles. Computer graphics animation and simulation help to find fundamental design errors at an early design stage and as this paper suggests, enable the user of the final product to take part in to the designing process of the robot controller. Benefits and difficulties of using computer graphics simulation in the wheelchair development process are discussed.     

RETRACTED ARTICLE: A multi-agent architectural solution for coherent distributed reconfigurations of function blocks

The paper deals with distributed Multi-Agent Reconfigurable Embedded Control Systems following the International Industrial Standard IEC61499 in which a Function Block (abbreviated by FB) is an event-triggered software component owning data and a control application is a network of distributed blocks that should satisfy functional and temporal properties according to user requirements. We define an architecture of reconfigurable multi-agent systems in which a Reconfiguration Agent is affected to each device of the execution environment to apply local reconfigurations, and a Coordination Agent is proposed for coordinations between devices in order to guarantee safe and adequate distributed reconfigurations. A Communication Protocol is proposed to handle coordinations between agents by using well-defined Coordination Matrices. We specify both reconfiguration agents to be modelled by nested state machines, and the Coordination Agent according to the formalism Net Condition-Event Systems (Abbreviated by NCES) which is an extension of Petri nets. To validate the whole architecture, we check by applying the model checker SESA in each device functional and temporal properties to be described according to the temporal logic “Computation Tree Logic”. We have also to check all possible coordinations between devices by verifying that whenever a reconfiguration is applied in a device, the Coordination Agent and other concerned devices react as described in user requirements. We present a tool applying simulations of this distributed architecture in order to check interactions and reactivities of agents. The paper’s contributions are applied to two Benchmark Production Systems available in our research laboratory.