Pages that link to "Item:Q4304492"
From MaRDI portal
The following pages link to Rewrite-based Equational Theorem Proving with Selection and Simplification (Q4304492):
Displaying 50 items.
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Paramodulation with non-monotonic orderings and simplification (Q352977) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- Model-theoretic methods in combined constraint satisfiability (Q556677) (← links)
- Redundancy criteria for constrained completion (Q673620) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Representing and building models for decidable subclasses of equational clausal logic (Q861367) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Deciding expressive description logics in the framework of resolution (Q924723) (← links)
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
- On the refutational completeness of signed binary resolution and hyperresolution (Q1037933) (← links)
- Completeness of hyper-resolution via the semantics of disjunctive logic programs (Q1041788) (← links)
- Superposition theorem proving for abelian groups represented as integer modules (Q1275020) (← links)
- Decidability and complexity analysis by basic paramodulation (Q1281494) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- Extracting models from clause sets saturated under semantic refinements of the resolution rule. (Q1401929) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- Hyperresolution for guarded formulae (Q1404983) (← links)
- On using ground joinable equations in equational theorem proving (Q1404987) (← links)
- Superposition with completely built-in abelian groups (Q1432887) (← links)
- Induction = I-axiomatization + first-order consistency. (Q1854350) (← links)
- Cancellative Abelian monoids and related structures in refutational theorem proving. I (Q1864898) (← links)
- Cancellative Abelian monoids and related structures in refutational theorem proving. II (Q1864899) (← links)
- Deciding the guarded fragments by resolution (Q1867216) (← links)
- A superposition calculus for abductive reasoning (Q2013317) (← links)
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) (Q2051565) (← links)
- Equational theorem proving modulo (Q2055853) (← links)
- Generalized completeness for SOS resolution and its application to a new notion of relevance (Q2055868) (← links)
- A unifying splitting framework (Q2055869) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
- Superposition for full higher-order logic (Q2055874) (← links)
- Neural precedence recommender (Q2055885) (← links)
- Improving ENIGMA-style clause selection while learning from history (Q2055886) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- Subsumption demodulation in first-order theorem proving (Q2096454) (← links)
- Larry Wos: visions of automated reasoning (Q2102922) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- An efficient subsumption test pipeline for BS(LRA) clauses (Q2104505) (← links)
- Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
- SCL(EQ): SCL for first-order logic with equality (Q2104511) (← links)
- AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
- Contradiction separation based dynamic multi-clause synergized automated deduction (Q2198231) (← links)
- Politeness and combination methods for theories with bridging functions (Q2303236) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
