The following pages link to (Q2751353):
Displaying 48 items.
- Extracting unsatisfiable cores for LTL via temporal resolution (Q266863) (← links)
- Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies (Q286087) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- The Ackermann approach for modal logic, correspondence theory and second-order reduction (Q420837) (← links)
- Consequence-based and fixed-parameter tractable reasoning in description logics (Q490523) (← links)
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- Enhancing unsatisfiable cores for LTL with information on temporal relevance (Q507378) (← links)
- Linearity and regularity with negation normal form (Q703486) (← links)
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- Binary resolution over Boolean lattices (Q853473) (← links)
- A clausal resolution method for branching-time logic \(\text{ECTL}^+\) (Q862827) (← 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)
- MetiTarski: An automatic theorem prover for real-valued special functions (Q972422) (← links)
- Tractable query answering and rewriting under description logic constraints (Q975872) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Labelled splitting (Q1037396) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- Completeness of hyper-resolution via the semantics of disjunctive logic programs (Q1041788) (← links)
- Deciding \(\mathcal H_1\) by resolution (Q1041797) (← links)
- Stratified resolution (Q1404977) (← links)
- Hyperresolution for guarded formulae (Q1404983) (← links)
- Limits of theory sequences over algebraically closed fields and applications. (Q1421482) (← links)
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators (Q1432885) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- A unifying splitting framework (Q2055869) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
- Confidences for commonsense reasoning (Q2055883) (← links)
- Neural precedence recommender (Q2055885) (← links)
- Improving ENIGMA-style clause selection while learning from history (Q2055886) (← links)
- Subsumption demodulation in first-order theorem proving (Q2096454) (← links)
- Layered clause selection for theory reasoning (short paper) (Q2096461) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- An efficient subsumption test pipeline for BS(LRA) clauses (Q2104505) (← links)
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL (Q2104508) (← links)
- Semantic relevance (Q2104509) (← links)
- GK: implementing full first order default logic for commonsense reasoning (system description) (Q2104518) (← links)
- The possibilistic Horn non-clausal knowledge bases (Q2105624) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- (Q5005105) (← links)
- (Q5111307) (← links)
- A first polynomial non-clausal class in many-valued logic (Q6083144) (← links)
- Unifying splitting (Q6103590) (← links)
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments (Q6149592) (← links)
- Superposition for higher-order logic (Q6156638) (← links)
