Cover Image

Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Kaufmann, Daniela, Berthomieu, Jérémy
Format:	Preprint
Published:	2024
Subjects:	Symbolic Computation Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formal Verification of Parameterized Systems based on Induction
by: Xiu, Jiaqi, et al.
Published: (2025)

130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
by: Urban, Josef
Published: (2026)

Solving unification in the description logic $\mathcal{FL}_\bot$
by: Morawska, Barbara, et al.
Published: (2024)

Rings with common division, common meadows and their conditional equational theories
by: Bergstra, Jan A, et al.
Published: (2024)

Improving NLSAT for Nonlinear Real Arithmetic
by: Wang, Zhonghan
Published: (2024)

Saturating Sorting without Sorts
by: Georgiou, Pamina, et al.
Published: (2024)

A Local Search Algorithm for MaxSMT(LIA)
by: He, Xiang, et al.
Published: (2024)

OSVAuto: automatic proofs about functional specifications in OS verification
by: Wu, Yulun, et al.
Published: (2024)

Exhaustive Symbolic Integration: Integration by Differentiation and the Landscape of Symbolic Integrability
by: Desmond, Harry
Published: (2026)

One-Parametric Presburger Arithmetic has Quantifier Elimination
by: Mansutti, Alessio, et al.
Published: (2025)

Proceedings of the 19th International Workshop on Logical and Semantic Frameworks, with Applications
by: Kop, Cynthia, et al.
Published: (2025)

Pseudo-Complex Quantifier Elimination
by: Faroß, Nicolas, et al.
Published: (2026)

Nominal Equational Rewriting and Narrowing
by: Ayala-Rincón, Mauricio, et al.
Published: (2025)

On Automating Proofs of Multiplier Adder Trees using the RTL Books
by: Manjrekar, Mayank
Published: (2025)

Structuring Definitions in Mathematical Libraries
by: Gusakov, Alena, et al.
Published: (2025)

SCL(FOL) Revisited
by: Bromberger, Martin, et al.
Published: (2023)

Frex: dependently-typed algebraic simplification
by: Allais, Guillaume, et al.
Published: (2023)

VeriFlow: Modeling Distributions for Neural Network Verification
by: Zaid, Faried Abu, et al.
Published: (2024)

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
by: Brown, Chad E., et al.
Published: (2026)

Efficient OWL2QL Meta-reasoning Using ASP-based Hybrid Knowledge Bases
by: Qureshi, Haya Majid, et al.
Published: (2025)

A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
by: Ding, Tianyi, et al.
Published: (2025)

Quantifier Elimination Meets Treewidth
by: Wu, Hao, et al.
Published: (2026)

Identity Testing for Radical Expressions
by: Balaji, Nikhil, et al.
Published: (2022)

On Ambiguity: The case of fraction, its meanings and roles
by: Bergstra, Jan A, et al.
Published: (2026)

Computing submatrices of the Hermite normal form of a structured polynomial matrix
by: Berthomieu, Jérémy, et al.
Published: (2026)

Relating the Computational and Logical Difficulty of Solving ODEs: From Polynomial to Discontinuous Right-Hand Sides
by: Bournez, Olivier, et al.
Published: (2026)

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
by: Kutsia, Temur, et al.
Published: (2024)

Linear equations with monomial constraints and decision problems in abelian-by-cyclic groups
by: Dong, Ruiwen
Published: (2024)

A Theoretical Review on Solving Algebra Problems
by: Yu, Xinguo, et al.
Published: (2024)

Practical Modelling with Bigraphs
by: Archibald, Blair, et al.
Published: (2024)

Boolean Matrix Logic Programming on the GPU
by: Ai, Lun
Published: (2024)

WebPie: A Tiny Slice of Dependent Typing
by: Scholliers, Christophe
Published: (2024)

Proceedings 13th International Workshop on Developments in Computational Models
by: Alves, Sandra, et al.
Published: (2024)

Routing and Scheduling in Answer Set Programming applied to Multi-Agent Path Finding: Preliminary Report
by: Kaminski, Roland, et al.
Published: (2024)

Towards Automatic Transformations of Coq Proof Scripts
by: Magaud, Nicolas
Published: (2024)

Integrating Fuzzy Logic into Deep Symbolic Regression
by: Gerdes, Wout, et al.
Published: (2024)

Automatic Generation of Polynomial Symmetry Breaking Constraints
by: Erascu, Madalina, et al.
Published: (2026)

Confluence of Conditional Rewriting Modulo
by: Lucas, Salvador
Published: (2025)

Semantic Properties of Computations Defined by Elementary Inference Systems
by: Lucas, Salvador
Published: (2025)

Scaling Neuro-symbolic Problem Solving: Solver-Free Learning of Constraints and Objectives
by: Defresne, Marianne, et al.
Published: (2025)