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.
- Model completeness, covers and superposition (Q2305411) (← links)
- Faster, higher, stronger: E 2.3 (Q2305435) (← links)
- Hyperresolution for Gödel logic with truth constants (Q2328910) (← links)
- A complete superposition calculus for primal grammars (Q2352496) (← links)
- Automated theorem proving by resolution in non-classical logics (Q2385426) (← links)
- Modular proof systems for partial functions with Evans equality (Q2432764) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Fault-Tolerant Aggregate Signatures (Q2798782) (← links)
- Selecting the Selection (Q2817931) (← links)
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (Q2817933) (← links)
- Agent-Based HOL Reasoning (Q2819202) (← links)
- A Generalisation of the Hyperresolution Principle to First Order Gödel Logic (Q2829667) (← links)
- On First-Order Model-Based Reasoning (Q2945706) (← links)
- A Rewriting Approach to the Combination of Data Structures with Bridging Theories (Q2964468) (← links)
- Modular Termination and Combinability for Superposition Modulo Counter Arithmetic (Q3172895) (← links)
- Congruence Closure with Free Variables (Q3303931) (← links)
- Beagle – A Hierarchic Superposition Theorem Prover (Q3454107) (← links)
- Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations (Q3455767) (← links)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties (Q3498479) (← links)
- Superposition for Fixed Domains (Q3540186) (← links)
- A term-graph clausal logic: completeness and incompleteness results ★ (Q3643364) (← links)
- Deciding the Inductive Validity of ∀ ∃ * Queries (Q3644758) (← links)
- Ordered tableaux: Extensions and applications (Q4610325) (← links)
- SPASS & FLOTTER version 0.42 (Q4647508) (← links)
- Theorem proving in cancellative abelian monoids (extended abstract) (Q4647536) (← links)
- Superposition for Bounded Domains (Q4913861) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- Canonical Ground Horn Theories (Q4916071) (← links)
- From Search to Computation: Redundancy Criteria and Simplification at Work (Q4916077) (← links)
- First-Order Resolution Methods for Modal Logics (Q4916086) (← links)
- A Resolution-based Model Building Algorithm for a Fragment of OCC1N = (Q4916224) (← links)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs (Q4916225) (← links)
- (Q4989394) (← links)
- Linking focusing and resolution with selection (Q5005105) (← links)
- Teaching Automated Theorem Proving by Example: PyRes 1.2 (Q5048999) (← links)
- Implementing Superposition in iProver (System Description) (Q5049017) (← links)
- Make E Smart Again (Short Paper) (Q5049019) (← links)
- Redundancy criteria for constrained completion (Q5055781) (← links)
- On narrowing, refutation proofs and constraints (Q5055818) (← links)
- Superposition theorem proving for abelian groups represented as integer modules (Q5055850) (← links)
- Local simplification (Q5096297) (← links)
- Buchberger's algorithm: A constraint-based completion procedure (Q5096314) (← links)
- (Q5140266) (← links)
- Decidability Results for Saturation-Based Model Building (Q5191116) (← links)
- Predicate Completion for non-Horn Clause Sets (Q5200033) (← links)
- Ordered chaining for total orderings (Q5210789) (← links)
- AC-superposition with constraints: No AC-unifiers needed (Q5210796) (← links)
- Semantic tableaux with ordering restrictions (Q5210807) (← links)
- Soft typing for ordered resolution (Q5234715) (← links)
- Automated Reasoning (Q5307048) (← links)
