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

Mathematics Subject Classification ID

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)

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

Cites Work

• scientific article; zbMATH DE number 3877456 (Why is no real title available?)
• scientific article; zbMATH DE number 3748394 (Why is no real title available?)
• scientific article; zbMATH DE number 827176 (Why is no real title available?)
• An introduction to many-valued and fuzzy logic. Semantics, algebras, and derivation systems
• Applying Linear Quantifier Elimination
• Automated Deduction – CADE-20
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• BI as an assertion language for mutable data structures
• Computer Aided Verification
• Decision Procedures for Multisets with Cardinality Constraints
• Effective Quantifier Elimination for Presburger Arithmetic with Infinity
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Interacting with Modal Logics in the Coq Proof Assistant
• Isabelle/HOL. A proof assistant for higher-order logic
• Linear Arithmetic with Stars
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic

Cited In (2)

• Reasoning about infinite computations
• Omega++

Uses Software

• Coq
• Isabelle/HOL
• HIP

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)