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