Certifying Proofs in the First-Order Theory of Rewriting

AbstractThe first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present , a reincarnation of the decision tool with certifiable output, and the formally verified certifier .

Download Full-text

A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439918 ◽

2021 ◽

Author(s):

Alexander Lochmann ◽

Aart Middeldorp ◽

Fabian Mitterwallner ◽

Bertram Felgenhauer

Keyword(s):

Decision Procedure ◽

Order Theory ◽

Rewrite Systems ◽

First Order ◽

First Order Theory

Download Full-text

Implementing the cylindrical algebraic decomposition within the Coq system

Mathematical Structures in Computer Science ◽

10.1017/s096012950600586x ◽

2007 ◽

Vol 17 (1) ◽

pp. 99-127 ◽

Cited By ~ 13

Author(s):

ASSIA MAHBOUBI

Keyword(s):

Programming Language ◽

Decision Procedure ◽

Order Theory ◽

Decomposition Algorithm ◽

Proof Assistant ◽

Real Numbers ◽

First Order ◽

Cylindrical Algebraic Decomposition ◽

First Order Theory ◽

Automation Tools

The Coq system is a Curry–Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.

Download Full-text

Prime models and almost decidability

Journal of Symbolic Logic ◽

10.1017/s0022481200031273 ◽

1986 ◽

Vol 51 (2) ◽

pp. 412-420 ◽

Cited By ~ 2

Author(s):

Terrence Millar

Keyword(s):

Order Theory ◽

The Other ◽

Prime Model ◽

First Order ◽

Decidable Theory ◽

Complete Extension ◽

First Order Theory ◽

Additional Constant ◽

Open Question ◽

Countable Models

This paper introduces and investigates a notion that approximates decidability with respect to countable structures. The paper demonstrates that there exists a decidable first order theory with a prime model that is not almost decidable. On the other hand it is proved that if a decidable complete first order theory has only countably many complete types, then it has a prime model that is almost decidable. It is not true that every decidable complete theory with only countably many complete types has a decidable prime model. It is not known whether a complete decidable theory with only countably many countable models up to isomorphism must have a decidable prime model. In [1] a weaker result was proven—if every complete extension, in finitely many additional constant symbols, of a theory T fails to have a decidable prime model, then T has 2ω nonisomorphic countable models. The corresponding statement for saturated models is false, even if all the complete types are recursive, as was shown in [2]. This paper investigates a variation of the open question via a different notion of effectiveness—almost decidable.A tree Tr will be a subset of ω<ω that is closed under predecessor. For elements f, g in ω<ω ∪ ωω, ƒ ⊲ g iffdf ∀i < lh(ƒ)[ƒ(i) = g(i)].

Download Full-text