Linear quantifier elimination
type: Item
instance of: scholarly article
title: Linear quantifier elimination
zbMATH Open document ID: 1207.68339
author: Tobias Nipkow
published in: Journal of Automated Reasoning
publication date: 2010-10-08T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03C10
zbMATH DE Number: 5797498
zbMATH Keywords: quantifier elimination
zbMATH Keywords: linear arithmetic
zbMATH Keywords: verification
describes a project that uses: Isabelle/HOL
MaRDI profile type: Publication
full work available at URL: s10817-010-9183-0
OpenAlex ID: W1971038681
Wikidata QID: Q56059277
cites work: Interpretation of Locales in Isabelle: Theories and Proof Contexts
cites work: Verifying Mixed Real-Integer Quantifier Elimination
cites work: Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
cites work: Q5674430
cites work: Q4052071
cites work: A Decision Procedure for the First Order Theory of Real Addition with Order
cites work: Q5302559
cites work: Constructive Type Classes in Isabelle
cites work: Q3618853
cites work: Applying Linear Quantifier Elimination
cites work: Automated Deduction – CADE-20
cites work: A Quantifier Elimination Algorithm for Linear Real Arithmetic
cites work: Q5760872
cites work: Linear Quantifier Elimination
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Complete Integer Decision Procedures as Derived Rules in HOL
cites work: Theorem Proving in Higher Order Logics
cites work: The complexity of linear problems in fields
DOI: 10.1007/S10817-010-9183-0
description: scientific article; zbMATH DE number 5797498