Pages that link to "Item:Q2751359"

The following pages link to Paramodulation-based theorem proving (Q2751359):

Displaying 50 items.

• Multi-completion with termination tools (Q352956) (← links)
• Paramodulation with non-monotonic orderings and simplification (Q352977) (← links)
• Model evolution with equality -- revised and implemented (Q429586) (← links)
• On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
• Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
• Automatic decidability and combinability (Q549666) (← links)
• Model-theoretic methods in combined constraint satisfiability (Q556677) (← links)
• Vampire with a brain is a good ITP hammer (Q831938) (← links)
• The disconnection tableau calculus (Q877889) (← links)
• Superposition-based equality handling for analytic tableaux (Q877891) (← links)
• Connection tableaux with lazy paramodulation (Q928656) (← links)
• A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
• Labelled splitting (Q1037396) (← links)
• A new methodology for developing deduction methods (Q1037405) (← links)
• Theory decision by decomposition (Q1041591) (← links)
• Combination of convex theories: modularity, deduction completeness, and explanation (Q1041593) (← links)
• Practical algorithms for deciding path ordering constraint satisfaction. (Q1400710) (← links)
• A rewriting approach to satisfiability procedures. (Q1401930) (← links)
• Stratified resolution (Q1404977) (← links)
• Superposition with completely built-in abelian groups (Q1432887) (← links)
• Superposition as a decision procedure for timed automata (Q1949086) (← 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)
• Neural precedence recommender (Q2055885) (← links)
• Improving ENIGMA-style clause selection while learning from history (Q2055886) (← links)
• A Knuth-Bendix-like ordering for orienting combinator equations (Q2096451) (← 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)
• An efficient subsumption test pipeline for BS(LRA) clauses (Q2104505) (← links)
• Ground joinability and connectedness in the superposition calculus (Q2104507) (← links)
• Semantic relevance (Q2104509) (← links)
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) (Q2104541) (← links)
• Automated generation of exam sheets for automated deduction (Q2128822) (← links)
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
• AC simplifications and closure redundancies in the superposition calculus (Q2142076) (← links)
• \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality (Q2156971) (← links)
• Contradiction separation based dynamic multi-clause synergized automated deduction (Q2198231) (← links)
• Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) (Q2238693) (← links)
• Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
• Combining induction and saturation-based theorem proving (Q2303240) (← links)
• Extending SMT solvers to higher-order logic (Q2305406) (← links)
• Model completeness, covers and superposition (Q2305411) (← links)
• Induction in saturation-based proof search (Q2305434) (← links)
• SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
• A complete superposition calculus for primal grammars (Q2352496) (← links)
• Tree automata with equality constraints modulo equational theories (Q2426520) (← links)
• Resolution with order and selection for hybrid logics (Q2429982) (← links)