Certified reasoning with infinity
DOI10.1007/978-3-319-19249-9_31zbMATH Open1427.68054OpenAlexW2293472070MaRDI QIDQ5206958FDOQ5206958
Authors: Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin 
Publication date: 19 December 2019
Published in: FM 2015: Formal Methods (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-19249-9_31
Recommendations
- Effective Quantifier Elimination for Presburger Arithmetic with Infinity
- Logic programming with infinite sets
- Reasoning about infinite computations
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Isabelle/HOL. A proof assistant for higher-order logic
- BI as an assertion language for mutable data structures
- An introduction to many-valued and fuzzy logic. Semantics, algebras, and derivation systems
- Title not available (Why is that?)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Computer Aided Verification
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Applying Linear Quantifier Elimination
- Automated Deduction – CADE-20
- Title not available (Why is that?)
- Interacting with Modal Logics in the Coq Proof Assistant
- Title not available (Why is that?)
- Decision Procedures for Multisets with Cardinality Constraints
- Linear Arithmetic with Stars
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Effective Quantifier Elimination for Presburger Arithmetic with Infinity
Cited In (2)
Uses Software
This page was built for publication: Certified reasoning with infinity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5206958)
