First-order automatic literal model generation
From MaRDI portal
Cites work
- A complete superposition calculus for primal grammars
- An Isabelle/HOL Formalization of the SCL(FOL) Calculus
- Automated model building
- BDI: a new decidable clause class
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Computing finite models by reduction to function-free clause logic
- Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints
- Decidability Results for Saturation-Based Model Building
- Deciding H₁ by resolution
- Deciding first-order satisfiability when universal and existential variables are separated
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Deciding the guarded fragments by resolution
- Exploring partial models with SCL
- Faster, higher, stronger: E 2.3
- First-order resolution methods for modal logics
- Handbook of satisfiability. In 2 parts
- scientific article; zbMATH DE number 5914361 (Why is no real title available?)
- scientific article; zbMATH DE number 1189060 (Why is no real title available?)
- scientific article; zbMATH DE number 1301755 (Why is no real title available?)
- scientific article; zbMATH DE number 1341618 (Why is no real title available?)
- scientific article; zbMATH DE number 1354167 (Why is no real title available?)
- scientific article; zbMATH DE number 512974 (Why is no real title available?)
- scientific article; zbMATH DE number 517065 (Why is no real title available?)
- scientific article; zbMATH DE number 515732 (Why is no real title available?)
- scientific article; zbMATH DE number 1140676 (Why is no real title available?)
- scientific article; zbMATH DE number 2043527 (Why is no real title available?)
- scientific article; zbMATH DE number 2090304 (Why is no real title available?)
- Hyperresolution and automated model building
- Model Representation over Finite and Infinite Signatures
- New results on rewrite-based satisfiability procedures
- On the saturation of YAGO
- On unification of terms with integer exponents
- Resolution decision procedures
- Resolution methods for the decision problem
- Resolution Strategies as Decision Procedures
- Schematic saturation for decision and unification problems.
- SCL clause learning from simple models
- SCL(EQ): SCL for first-order logic with equality
- Superposition for bounded domains
- Towards Smarter MACE-style Model Finders
This page was built for publication: First-order automatic literal model generation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034872)
