Exploring partial models with SCL

DOI10.29007/8BR1MaRDI QIDQ7025227zbMATH OpenFDO

Authors Martin Bromberger, Simon Schwarz, Christoph Weidenbach

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/8BR1

zbMATH Keywords

first-order reasoningSCLfirst-order model buildingnon-redundant learning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 1189096 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Deciding effectively propositional logic using DPLL and substitution sets
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Finding Finite Models in Multi-sorted First-Order Logic
• Lemma Learning in the Model Evolution Calculus
• Model Representation over Finite and Infinite Signatures
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• On First-Order Model-Based Reasoning
• Paramodulation-based theorem proving
• Proof Systems for Effectively Propositional Logic
• Resolution theorem proving
• SCL clause learning from simple models
• SCL(EQ): SCL for first-order logic with equality
• Semantically-guided goal-sensitive reasoning: model representation
• Short proofs without new variables
• Towards Smarter MACE-style Model Finders

Cited in

(1)

• First-order automatic literal model generation

This page was built for publication: Exploring partial models with SCL

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