Rewrite-based Equational Theorem Proving with Selection and Simplification
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
- Superposition with Delayed Unification
- Verified Given Clause Procedures
- Extending SMT solvers to higher-order logic
- Ground joinability and connectedness in the superposition calculus
- Modular proof systems for partial functions with Evans equality
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- First-order resolution methods for modal logics
- Disproving using the inverse method by iterative refinement of finite approximations
- Semantic tableaux with ordering restrictions
- A first polynomial non-clausal class in many-valued logic
- Linking focusing and resolution with selection
- SAT solving for variants of first-order subsumption
- Predicate Completion for non-Horn Clause Sets
- Controlled use of clausal lemmas in connection tableau calculi
- Hyperresolution for Gödel logic with truth constants
- SAT-Inspired Eliminations for Superposition
- Clause set cycles and induction
- A unifying splitting framework
- Agent-based HOL reasoning
- Beagle -- a hierarchic superposition theorem prover
- Soft typing for ordered resolution
- Redundancy criteria for constrained completion
- Make E Smart Again (Short Paper)
- Equational Theorem Proving for Clauses over Strings
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Redundancy criteria for constrained completion
- Combining induction and saturation-based theorem proving
- SPASS \& FLOTTER version 0.42
- On narrowing, refutation proofs and constraints
- Blocking and other enhancements for bottom-up model generation methods
- Faster, higher, stronger: E 2.3
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- An efficient subsumption test pipeline for BS(LRA) clauses
- SCL(EQ): SCL for first-order logic with equality
- AC simplifications and closure redundancies in the superposition calculus
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Superposition for Fixed Domains
- Superposition with lambdas
- SAT-Inspired Higher-Order Eliminations
- SCL(EQ): SCL for first-order logic with equality
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- On the refutational completeness of signed binary resolution and hyperresolution
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Canonical ground Horn theories
- Deciding expressive description logics in the framework of resolution
- Modular termination and combinability for superposition modulo counter arithmetic
- scientific article; zbMATH DE number 4045219 (Why is no real title available?)
- On using ground joinable equations in equational theorem proving
- A term-graph clausal logic: completeness and incompleteness results ★
- A Generalisation of the Hyperresolution Principle to First Order Gödel Logic
- Extensional higher-order paramodulation in Leo-III
- Equational theorem proving modulo
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Theorem proving in cancellative abelian monoids (extended abstract)
- A superposition calculus for abductive reasoning
- Harald Ganzinger's legacy: contributions to logics and programming
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Towards automated deduction in cP systems
- Semantically-guided goal-sensitive reasoning: model representation
- Buchberger's algorithm: a constraint-based completion procedure
- Model-theoretic methods in combined constraint satisfiability
- Fault-tolerant aggregate signatures
- Ordered tableaux: extensions and applications
- An instantiation scheme for satisfiability modulo theories
- On deciding satisfiability by theorem proving with speculative inferences
- Superposition for bounded domains
- Performance of clause selection heuristics for saturation-based theorem proving
- Representing and building models for decidable subclasses of equational clausal logic
- A rewriting approach to the combination of data structures with bridging theories
- Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
- Ordered chaining for total orderings
- Congruence closure with free variables
- Some techniques for reasoning automatically on co-inductive data structures
- A complete superposition calculus for primal grammars
- Improving ENIGMA-style clause selection while learning from history
- Local simplification
- A combinator-based superposition calculus for higher-order logic
- Superposition theorem proving for abelian groups represented as integer modules
- Selecting the selection
- Equational theorem proving for clauses over strings
- A comprehensive framework for saturation theorem proving
- Superposition with lambdas
- Superposition with completely built-in abelian groups
- Automatic bit- and memory-precise verification of eBPF code
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Politeness and combination methods for theories with bridging functions
- Superposition for higher-order logic
- Hyperresolution for guarded formulae
- Superposition-based equality handling for analytic tableaux
- The disconnection tableau calculus
- On the (in-)completeness of destructive equality resolution in the superposition calculus
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Subsumption demodulation in first-order theorem proving
- A rewriting approach to satisfiability procedures.
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Induction = I-axiomatization + first-order consistency.
- A strict constrained superposition calculus for graphs
This page was built for publication: Rewrite-based Equational Theorem Proving with Selection and Simplification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4304492)
