Proof synthesis and reflection for linear arithmetic
type: Item
instance of: scholarly article
title: Proof synthesis and reflection for linear arithmetic
zbMATH Open document ID: 1171.03006
author: Amine Chaieb
author: Tobias Nipkow
published in: Journal of Automated Reasoning
publication date: 2008-09-10T00:00:00Z
review text: The authors present an implementation of quantifier elimination for integer and linear arithmetic. The algorithms (those by Cooper for \({\mathbb Z}\) and by Ferrante and Rackoff for \({\mathbb R}\)) are realized in two different ways: one \textit{in a tactic style}, by a proof producing a functional program, and the other one \textit{by reflection}, i.e.\ by computations inside the logic. The methods are compared using an implementation in Isabelle/HOL; it is noted that the implementation using the reflective approach is faster.
reviewed by: Viorica Sofronie-Stokkermans
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03C10
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5324394
zbMATH Keywords: proof synthesis
zbMATH Keywords: reflection
zbMATH Keywords: linear arithmetic
zbMATH Keywords: quantifier elimination
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL
describes a project that uses: Coq
describes a project that uses: ML
MaRDI profile type: Publication
full work available at URL: s10817-008-9101-x
OpenAlex ID: W2056972299
cites work: Autarkic computations in formal proofs
cites work: Q4736387
cites work: The complexity of logical theories
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Verifying Mixed Real-Integer Quantifier Elimination
cites work: Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
cites work: Alternation
cites work: Q4079605
cites work: Q5674430
cites work: Q4052071
cites work: A Decision Procedure for the First Order Theory of Real Addition with Order
cites work: Q4082296
cites work: The complexity of Presburger arithmetic with bounded quantifier alternation depth
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q5287513
cites work: Subclasses of Presburger arithmetic and the polynomial-time hierarchy
cites work: A compiled implementation of strong reduction
cites work: Q4231030
cites work: Validated proof-producing decision procedures
cites work: Applying Linear Quantifier Elimination
cites work: An Interpretation of Isabelle/HOL in HOL Light
cites work: Automated Deduction – CADE-20
cites work: Q5760872
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Complete Integer Decision Procedures as Derived Rules in HOL
cites work: Q4063432
cites work: Logic and Computation
cites work: Presburger arithmetic with bounded quantifier alternation
cites work: Complexity of Subcases of Presburger Arithmetic
cites work: Q5807665
cites work: The complexity of linear problems in fields
cites work: The complexity of almost linear diophantine problems
cites work: Q4226937
DOI: 10.1007/S10817-008-9101-X
description: scientific article; zbMATH DE number 5324394