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.

On the arithmetic of theorem proving

We present the arithmetization of strings in order to be deployed as an alternative model for automatic theorem proving.

Using prime numbers for automatic theorem proving

We apply an analogous setting from Gödel's numbering system to automatic theorem proving.

PCF-based formalization of the parallel composition of automata

The paper demonstrates how the automatic theorem proving technique of the PCF calculus is applied to construct parallel composition of automata. Parallel composition plays an essential role in the supervisory control theory at different stages of systems and supervisors design. Improved formalization of discrete event systems as positively-constructed formulas along with auxiliary predicates, serving for accessibility of the automaton checking, simplify parallel composition construction.

ON THE NUMBER OF ABELIAN BORDERED WORDS (WITH AN EXAMPLE OF AUTOMATIC THEOREM-PROVING)

In the literature, many bijections between (labeled) Motzkin paths and various other combinatorial objects are studied. We consider abelian (un)bordered words and show the connection with irreducible symmetric Motzkin paths and paths in ℤ not returning to the origin. This study can be extended to abelian unbordered words over an arbitrary alphabet and we derive expressions to compute the number of these words. In particular, over a 3-letter alphabet, the connection with paths in the triangular lattice is made. Finally, we characterize the lengths of the abelian unbordered factors occurring in the Thue–Morse word using some kind of automatic theorem-proving provided by a logical characterization of the k-automatic sequences.

Modeling and Reasoning about States in Late Launch Based on Horn Clauses

Late Launch, which is a kind of dynamic measurement technology proposed by both Intel and AMD, offers isolated execution environment for codes needed to be protected. However, since the specifications and documents of Late Launch have hundreds of pages, they are too long and complicated to be fully covered and analyzed. A model based on Horn clauses is presented to solve the problem that there is a lack of realistic models and of automated tools for the verification of security protocols based on Late Launch. A running example is taken to show the execution details of Late Launch. Based on the example, secrecy properties of Late Launch are verified. Whats more, the automatic theorem proving tool ProVerif is used to make the verification more fast and accurate.

AUTOMATIC THEOREM-PROVING IN COMBINATORICS ON WORDS

We describe a technique for mechanically proving certain kinds of theorems in combinatorics on words, using finite automata and a software package for manipulating them. We illustrate our technique by applying it to (a) solve an open problem of Currie and Saari on the lengths of unbordered factors in the Thue-Morse sequence; (b) verify an old result of Prodinger and Urbanek on the regular paperfolding sequence; (c) find an explicit expression for the recurrence function for the Rudin-Shapiro sequence; and (d) improve the avoidance bound in Leech's squarefree sequence. We also introduce a new measure of infinite words called condensation and compute it for some famous sequences. We follow up on the study of Currie and Saari of least periods of infinite words. We show that the characteristic sequence of least periods of a k-automatic sequence is (effectively) k-automatic. We compute the least periods for several famous sequences. Many of our results were obtained by machine computations.