Cover Image

SAT-Inspired Higher-Order Eliminations

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Blanchette, Jasmin, Vukmirović, Petar
Format:	Preprint
Published:	2022
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Optimistic Higher-Order Superposition
by: Bentkamp, Alexander, et al.
Published: (2025)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
by: Bartl, Lukas, et al.
Published: (2025)

Term Orders for Optimistic Lambda-Superposition
by: Bentkamp, Alexander, et al.
Published: (2025)

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

SAT Solving for Variants of First-Order Subsumption
by: Coutelier, Robin, et al.
Published: (2024)

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
by: Bacci, Giorgio, et al.
Published: (2025)

RustSAT: A Library For SAT Solving in Rust
by: Jabs, Christoph
Published: (2025)

Learning to Rank the Initial Branching Order of SAT Solvers
by: Eriksson, Arvid, et al.
Published: (2026)

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

Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving
by: Shi, Zhengyuan, et al.
Published: (2024)

Hammering Higher Order Set Theory
by: Brown, Chad E., et al.
Published: (2025)

Kuroda's Translation for Higher-Order Logic
by: Traversié, Thomas
Published: (2024)

SAT-Based Subsumption Resolution
by: Coutelier, Robin, et al.
Published: (2024)

Life span of SAT techniques
by: Fleury, Mathias, et al.
Published: (2024)

Higher Order Automatic Differentiation of Higher Order Functions
by: Huot, Mathieu, et al.
Published: (2021)

Syntactic Effectful Realizability in Higher-Order Logic
by: Cohen, Liron, et al.
Published: (2025)

Between proof construction and SAT-solving
by: Schubert, Aleksy, et al.
Published: (2024)

The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)
by: Niederhauser, Johannes, et al.
Published: (2025)

Free Monads, Intrinsic Scoping, and Higher-Order Preunification
by: Kudasov, Nikolai
Published: (2022)

Higher-Order Constrained Dependency Pairs for (Universal) Computability
by: Guo, Liye, et al.
Published: (2024)

Unification of Deterministic Higher-Order Patterns (Full Version)
by: Niederhauser, Johannes, et al.
Published: (2026)

Expectation-based Analysis of Higher-Order Quantum Programs
by: Avanzini, Martin, et al.
Published: (2025)

Big Steps in Higher-Order Mathematical Operational Semantics
by: Goncharov, Sergey, et al.
Published: (2025)

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

Compact SAT Encoding for Power Peak Minimization
by: Van Kieu, Tuyen, et al.
Published: (2025)

Empirical Impact of Dimensionality on Random Geometric SAT
by: Rädiker, Flora
Published: (2026)

SAT-based Learning of Computation Tree Logic
by: Pommellet, Adrien, et al.
Published: (2024)

Equilibrium Semantics and Strong Equivalence for Higher-Order Logic Programs
by: Charalambidis, Angelos, et al.
Published: (2026)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
by: Feng, Nick, et al.
Published: (2024)

SAT-Based Techniques for Lexicographically Smallest Finite Models
by: Janota, Mikoláš, et al.
Published: (2025)

parSAT: Parallel Solving of Floating-Point Satisfiability
by: Krahl, Markus, et al.
Published: (2025)

Approaching the Conway-99 problem using SAT solvers
by: Keramatipour, Ali
Published: (2026)

Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security
by: Kammüller, Florian
Published: (2023)

Higher-Order Weakest Precondition Transformers via a CPS Transformation
by: Kura, Satoshi
Published: (2023)

A Category-Theoretic Perspective on Higher-Order Approximation Fixpoint Theory
by: Pollaci, Samuele, et al.
Published: (2024)

Higher-Order Asynchronous Effects
by: Ahman, Danel, et al.
Published: (2023)

Certified Branch-and-Bound MaxSAT Solving (Extended Version)
by: Vandesande, Dieter, et al.
Published: (2025)

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

SAT Encodings for Bandwidth Coloring: A Systematic Design Study
by: Nguyen, Duc Trung Kim, et al.
Published: (2026)

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