Computing small clause normal forms
From MaRDI portal
Recommendations
Cited in
(54)- Exploiting conjunctive queries in description logic programs
- Labelled splitting
- An analog of the Cook theorem for polytopes
- Superposition with first-class booleans and inprocessing clausification
- Neural precedence recommender
- Semantic relevance
- Making theory reasoning simpler
- Incremental search for conflict and unit instances of quantified formulas with E-matching
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- Combining induction and saturation-based theorem proving
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
- SPASS-SATT. A CDCL(LA) solver
- Induction in saturation-based proof search
- Faster, higher, stronger: E 2.3
- Extending Sledgehammer with SMT solvers
- HermiT: an OWL 2 reasoner
- Automation for interactive proof: first prototype
- Reasoning in description logics by a reduction to disjunctive datalog
- Extended resolution simulates binary decision diagrams
- Translation of resolution proofs into short first-order proofs without choice axioms
- Mechanising first-order temporal resolution
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Effective normalization techniques for HOL
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Second-order quantifier elimination on relational monadic formulas -- a basic method and some less expected applications
- Case splitting in an automatic theorem prover for real-valued special functions
- scientific article; zbMATH DE number 404251 (Why is no real title available?)
- scientific article; zbMATH DE number 1303351 (Why is no real title available?)
- Combining decision procedures by (model-)equality propagation
- scientific article; zbMATH DE number 1948188 (Why is no real title available?)
- Public announcements, public assignments and the complexity of their logic
- Temporal equilibrium logic with past operators
- Reasoning about norms under uncertainty in dynamic environments
- Theorem proving in large formal mathematics as an emerging AI field
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Computing Tiny Clause Normal Forms
- Extending Sledgehammer with SMT solvers
- MPTP-motivation, implementation, first experiments
- SAT-Inspired Eliminations for Superposition
- Making higher-order superposition work
- Making higher-order superposition work
- Scalable fine-grained proofs for formula processing
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
- Superposition for higher-order logic
- Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)
- On Incremental Pre-processing for SMT
- Quantifier shifting for quantified Boolean formulas revisited
- Optimizing the clausal normal form transformation
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Semantic forgetting in expressive description logics
- Applying SAT solving in classification of finite algebras
- HySAT: An efficient proof engine for bounded model checking of hybrid systems
- Deciding expressive description logics in the framework of resolution
- Resolution is cut-free
This page was built for publication: Computing small clause normal forms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751358)
