Cover Image

Partial Quantifier Elimination By Certificate Clauses

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Goldberg, Eugene
Format:	Preprint
Published:	2020
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

On Efficient Algorithms For Partial Quantifier Elimination
by: Goldberg, Eugene
Published: (2024)

Structure-Aware Computing, Partial Quantifier Elimination And SAT
by: Goldberg, Eugene
Published: (2024)

Solving SAT By Computing A Stable Set Of Points In Clusters
by: Goldberg, Eugene
Published: (2025)

Property Checking Without Inductive Invariants
by: Goldberg, Eugene
Published: (2016)

Disjoint Partial Enumeration without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2023)

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

Integer Linear-Exponential Programming in NP by Quantifier Elimination
by: Chistikov, Dmitry, et al.
Published: (2024)

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
by: Ratschan, Stefan, et al.
Published: (2026)

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

Quantifier Elimination and Craig Interpolation, Quantitatively
by: Batz, Kevin, et al.
Published: (2025)

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
by: Amat, Nicolas, et al.
Published: (2024)

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

Rethinking Clause Management for CDCL SAT Solvers
by: Cai, Yalun, et al.
Published: (2026)

Equational Theorem Proving for Clauses over Strings
by: Kim, Dohan
Published: (2023)

On the Cut Elimination of Weak Intuitionistic Tense Logic
by: Wang, Yiheng, et al.
Published: (2024)

On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
by: Beutner, Raven, et al.
Published: (2025)

CTL* Verification and Synthesis using Existential Horn Clauses
by: Carelli, Mishel, et al.
Published: (2024)

Testing for Renamability to Classes of Clause Sets
by: Brandl, Albert, et al.
Published: (2025)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2024)

Extended Resolution Clause Learning via Dual Implication Points
by: Buss, Sam, et al.
Published: (2024)

Efficient Neural Clause-Selection Reinforcement
by: Suda, Martin
Published: (2025)

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
by: Katsura, Hiroyuki, et al.
Published: (2025)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
by: De Angelis, Emanuele, et al.
Published: (2024)

Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
by: Lichtner, Kilian, et al.
Published: (2025)

The Dual of Quantifier Elimination: Boolean Elimination over C and R
by: Frank, Matthew
Published: (2025)

Embedded Finite Models Beyond Restricted Quantifier Collapse
by: Benedikt, Michael, et al.
Published: (2023)

Some General Completeness Results for Propositionally Quantified Modal Logics
by: Ding, Yifeng, et al.
Published: (2024)

SAT-Inspired Higher-Order Eliminations
by: Blanchette, Jasmin, et al.
Published: (2022)

Cut-Elimination for the Bimodal Logic GR
by: Kushida, Hirohiko
Published: (2026)

IMELL Cut Elimination with Linear Overhead
by: Accattoli, Beniamino, et al.
Published: (2024)

Goedel Logics: On the Elimination of The Absoluteness Operator
by: Baaz, Matthias, et al.
Published: (2026)

Complete $ω$-Regular Supermartingale Certificates
by: Abate, Alessandro, et al.
Published: (2026)

PICID: Proof-Driven Clause Learning in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

On Symbol Elimination and Uniform Interpolation in Theory Extensions
by: Sofronie-Stokkermans, Viorica
Published: (2025)

Eliminating reversals from cubical type theories
by: Cavallo, Evan, et al.
Published: (2026)

Satisfiability Modulo Theories for Verifying MILP Certificates
by: Wood, Kenan, et al.
Published: (2023)

Visualizing Game-Based Certificates for Hyperproperty Verification
by: Beutner, Raven, et al.
Published: (2025)

Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
by: Lyon, Tim S., et al.
Published: (2026)

The Proof-Theoretic Origin of Double Negation Introduction & Elimination
by: Irani, Khashayar
Published: (2025)

Variable Elimination as Rewriting in a Linear Lambda Calculus
by: Ehrhard, Thomas, et al.
Published: (2025)