Rewrite-based Equational Theorem Proving with Selection and Simplification
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- On the refutational completeness of signed binary resolution and hyperresolution
- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- Superposition theorem proving for abelian groups represented as integer modules
- Decidability and complexity analysis by basic paramodulation
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- A rewriting approach to satisfiability procedures.
- Hyperresolution for guarded formulae
- On using ground joinable equations in equational theorem proving
- Superposition with completely built-in abelian groups
- Induction = I-axiomatization + first-order consistency.
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- Deciding the guarded fragments by resolution
- A superposition calculus for abductive reasoning
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Equational theorem proving modulo
- Generalized completeness for SOS resolution and its application to a new notion of relevance
- A unifying splitting framework
- Superposition with first-class booleans and inprocessing clausification
- Superposition for full higher-order logic
- Neural precedence recommender
- Improving ENIGMA-style clause selection while learning from history
- A combinator-based superposition calculus for higher-order logic
- Subsumption demodulation in first-order theorem proving
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- An efficient subsumption test pipeline for BS(LRA) clauses
- Ground joinability and connectedness in the superposition calculus
- SCL(EQ): SCL for first-order logic with equality
- AC simplifications and closure redundancies in the superposition calculus
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Politeness and combination methods for theories with bridging functions
- Blocking and other enhancements for bottom-up model generation methods
- Combining induction and saturation-based theorem proving
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Extending SMT solvers to higher-order logic
- Model completeness, covers and superposition
- Faster, higher, stronger: E 2.3
- Hyperresolution for Gödel logic with truth constants
- A complete superposition calculus for primal grammars
- Automated theorem proving by resolution in non-classical logics
- Modular proof systems for partial functions with Evans equality
- Extensional higher-order paramodulation in Leo-III
- Fault-tolerant aggregate signatures
- Selecting the selection
- Performance of clause selection heuristics for saturation-based theorem proving
- Agent-based HOL reasoning
- A Generalisation of the Hyperresolution Principle to First Order Gödel Logic
- Semantically-guided goal-sensitive reasoning: model representation
- On First-Order Model-Based Reasoning
- A rewriting approach to the combination of data structures with bridging theories
- Modular termination and combinability for superposition modulo counter arithmetic
- Congruence closure with free variables
- Beagle -- a hierarchic superposition theorem prover
- Disproving using the inverse method by iterative refinement of finite approximations
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Paramodulation with non-monotonic orderings and simplification
- Superposition for Fixed Domains
- A term-graph clausal logic: completeness and incompleteness results ★
- Deciding the Inductive Validity of ∀ ∃ * Queries
- scientific article; zbMATH DE number 4045219 (Why is no real title available?)
- scientific article; zbMATH DE number 1231675 (Why is no real title available?)
- On deciding satisfiability by theorem proving with speculative inferences
- An instantiation scheme for satisfiability modulo theories
- Ordered tableaux: extensions and applications
- SPASS \& FLOTTER version 0.42
- Theorem proving in cancellative abelian monoids (extended abstract)
- Superposition for bounded domains
- Harald Ganzinger's legacy: contributions to logics and programming
- Canonical ground Horn theories
- From search to computation: redundancy criteria and simplification at work
- First-order resolution methods for modal logics
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Superposition for lambda-free higher-order logic
- Linking focusing and resolution with selection
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Implementing Superposition in iProver (System Description)
- Make E Smart Again (Short Paper)
- Redundancy criteria for constrained completion
- On narrowing, refutation proofs and constraints
- Superposition theorem proving for abelian groups represented as integer modules
- Local simplification
- Buchberger's algorithm: a constraint-based completion procedure
- Clause set cycles and induction
- Decidability Results for Saturation-Based Model Building
- Predicate Completion for non-Horn Clause Sets
- Ordered chaining for total orderings
- AC-superposition with constraints: no AC-unifiers needed
- Semantic tableaux with ordering restrictions
- Soft typing for ordered resolution
- Automated Reasoning
- Model-theoretic methods in combined constraint satisfiability
- SAT-Inspired Eliminations for Superposition
- Superposition with lambdas
- A comprehensive framework for saturation theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Superposition with lambdas
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)
