SAT solving for variants of first-order subsumption

DOI10.1007/S10703-024-00454-1MaRDI QIDQ6911405zbMATH OpenFDO

Authors Jakob Rath, Michael G. Rawson, Armin Biere, Laura Kovács

Publication date 24 October 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10703-024-00454-1

zbMATH Keywords

first-order theorem provingSAT solvingsaturationsubsumption

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• AVATAR: The Architecture for First-Order Theorem Provers
• Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
• Cadiback: Extracting backbones with CaDiCaL
• Deep learning
• Fast approximations of quantifier elimination
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 3945370 (Why is no real title available?)
• scientific article; zbMATH DE number 4049047 (Why is no real title available?)
• scientific article; zbMATH DE number 1765674 (Why is no real title available?)
• Meta-F\textsuperscript{\(\star\)}: proof automation with SMT, tactics, and metaprograms
• Mining definitions in Kissat with Kittens
• On the efficiency of subsumption algorithms
• On the Implementation of Weight Constraint Rules in Conflict-Driven ASP Solvers
• Paramodulation-based theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SAT-Based Subsumption Resolution
• Scikit-learn: machine learning in Python
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• SMT-based model checking for recursive programs
• Strong extension-free proof systems
• Subsumption demodulation in first-order theorem proving
• Superposition with structural induction
• Term indexing
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

This page was built for publication: SAT solving for variants of first-order subsumption

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6911405)