Pages that link to "Item:Q2751358"
From MaRDI portal
The following pages link to Computing small clause normal forms (Q2751358):
Displaying 49 items.
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- Reasoning about norms under uncertainty in dynamic environments (Q465604) (← links)
- MPTP-motivation, implementation, first experiments (Q556682) (← links)
- Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) (Q631075) (← links)
- Optimizing the clausal normal form transformation (Q809622) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Semantic forgetting in expressive description logics (Q831928) (← links)
- Applying SAT solving in classification of finite algebras (Q862393) (← links)
- HySAT: An efficient proof engine for bounded model checking of hybrid systems (Q883144) (← links)
- Deciding expressive description logics in the framework of resolution (Q924723) (← links)
- Resolution is cut-free (Q972424) (← links)
- Exploiting conjunctive queries in description logic programs (Q1028641) (← links)
- Labelled splitting (Q1037396) (← links)
- An analog of the Cook theorem for polytopes (Q1759309) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
- Neural precedence recommender (Q2055885) (← links)
- Semantic relevance (Q2104509) (← links)
- Making theory reasoning simpler (Q2233504) (← links)
- Incremental search for conflict and unit instances of quantified formulas with E-matching (Q2234102) (← links)
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) (Q2238693) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments (Q2303247) (← links)
- SPASS-SATT. A CDCL(LA) solver (Q2305409) (← links)
- Induction in saturation-based proof search (Q2305434) (← links)
- Faster, higher, stronger: E 2.3 (Q2305435) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- HermiT: an OWL 2 reasoner (Q2351420) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Reasoning in description logics by a reduction to disjunctive datalog (Q2462648) (← links)
- Extended resolution simulates binary decision diagrams (Q2478427) (← links)
- Translation of resolution proofs into short first-order proofs without choice axioms (Q2486578) (← links)
- Mechanising first-order temporal resolution (Q2486579) (← links)
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification (Q2629858) (← links)
- Effective Normalization Techniques for HOL (Q2817937) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Q3455775) (← links)
- Public announcements, public assignments and the complexity of their logic (Q4583171) (← links)
- Temporal Equilibrium Logic with past operators (Q4586227) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs (Q4916225) (← links)
- Computing Tiny Clause Normal Forms (Q4928432) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- SAT-Inspired Eliminations for Superposition (Q5875949) (← links)
- Making higher-order superposition work (Q5918403) (← links)
- Making higher-order superposition work (Q5918575) (← links)
- Scalable fine-grained proofs for formula processing (Q5919479) (← links)
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments (Q6149592) (← links)
- Superposition for higher-order logic (Q6156638) (← links)
