Proof synthesis and reflection for linear arithmetic

DOI10.1007/s10817-008-9101-xzbMath1171.03006OpenAlexW2056972299MaRDI QIDQ945055

Amine Chaieb, Tobias Nipkow

Publication date: 10 September 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-008-9101-x

zbMATH Keywords

reflectionquantifier eliminationlinear arithmeticproof synthesis

Mathematics Subject Classification ID

Related Items (4)

A heuristic prover for real inequalities ⋮ Formalizing the Logic-Automaton Connection ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Incorporating quotation and evaluation into Church's type theory

Uses Software

• Coq
• ML
• Isabelle/HOL
• HOL

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The complexity of almost linear diophantine problems
• The complexity of linear problems in fields
• Subclasses of Presburger arithmetic and the polynomial-time hierarchy
• The complexity of logical theories
• The complexity of Presburger arithmetic with bounded quantifier alternation depth
• Isabelle/HOL. A proof assistant for higher-order logic
• Autarkic computations in formal proofs
• Edinburgh LCF. A mechanized logic of computation
• A compiled implementation of strong reduction
• Applying Linear Quantifier Elimination
• Complexity of Subcases of Presburger Arithmetic
• Complete Integer Decision Procedures as Derived Rules in HOL
• An Interpretation of Isabelle/HOL in HOL Light
• Verifying Mixed Real-Integer Quantifier Elimination
• Logic and Computation
• Alternation
• A Decision Procedure for the First Order Theory of Real Addition with Order
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• Automated Deduction – CADE-20
• Presburger arithmetic with bounded quantifier alternation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof synthesis and reflection for linear arithmetic