Narrow Results

In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs.

This paper focuses on the formal proof of parallel programs dedicated to distributed memory symmetric interconnection networks; communications are realized by message passing. We have developed a method to formally verify the computational correctness of this kind of application. Using the notion of Cayley graphs to model the networks in the Nqthm theorem prover, we have formally specified and mechanically proven correct a large set of collective communication primitives. Our compositional approach allows us to reuse these libraries of pre-proven procedures to validate complex application programs within Nqthm. This is illustrated by three examples.

We study the validation of implementation models of memory consistency protocols. Memory consistency protocols are modeled as transition systems and we use the methodology of refinements to validate a model against a specification. To automate the proof of such refinements, we propose a syntactic extension to the S1S decidable logic.

This article shows a novel program analysis framework based on Lewis' theory of counterfactuals. Using this framework we are capable of performing change-impact static analysis on a program's source code. In other words, we are able to prove the properties induced by changes to a given program before applying these changes. Our contribution is two-fold; we show how to use Lewis' logic of counterfactuals to prove that proposed changes to a program preserve its correctness. We report the development of an automated tool based on resolution and theorem proving for performing code change-impact analysis.

Automated Theorem Proving (ATP) is hard research of automated reasoning. The inference mechanism of most state-of-the-art first-order theorem provers is essentially a binary resolution method. The resolution method involves two clauses, and generates a clause with many literals in every deduction step, the search space will explode very quickly. Multi-clause standard contradiction separation (S-CS) calculus for first-order logic as a breakthrough of automated reasoning can restrict limitations. Based on S-CS rule, we propose a novel method called complementary ratio in this paper. Complementary ratio then is integrated into the leading ATP system Vampire, and we test the CASC-28 competition theorems (FOF division). The results show that complementary ratio can improve the performance of CS-based prover and Vampire.

Because of the large number of strategies and inference rules presently under consideration in automated theorem proving, there is a need for developing a language especially oriented toward automated theorem proving. This paper discusses some of the features and instructions of this language. The use of this language permits easy extension of automated theorem-proving programs to include new strategies and/or new inference rules. Such extendability will permit general experimentation with the various alternative systems.

In this article, we tell a story of good fortune. The good fortune concerns the discovery of a systematic approach to compress fifty years of excellent research in logic into a single day's use of an automated reasoning program. The discovery resulted from a colleague's experiment with a new representation and a new use of the weighting strategy. The experiment focused on an attempt—which I knew would fail—to prove one of the benchmark theorems that had eluded us for years. Fortunately, I was wrong; my colleague's attempt was successful, and a proof was found. That proof led to proving in one day thirteen theorems, theorems that resulted from fifty years of excellent research in logic. We present these theorems as intriguing problems to test the power of a reasoning program or to evaluate the effectiveness of a new idea. In addition to the challenge problems, we discuss a possible approach to finding shorter proofs and the results achieved with it.