Pages that link to "Item:Q1328182"
From MaRDI portal
The following pages link to Refutational theorem proving for hierarchic first-order theories (Q1328182):
Displayed 36 items.
- The Ackermann approach for modal logic, correspondence theory and second-order reduction (Q420837) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- A combined superposition and model evolution calculus (Q438531) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Symbol elimination and applications to parametric entailment problems (Q831921) (← links)
- Cancellative Abelian monoids and related structures in refutational theorem proving. I (Q1864898) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- Superposition decides the first-order logic fragment over ground theories (Q1949088) (← links)
- A superposition calculus for abductive reasoning (Q2013317) (← links)
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420) (← links)
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) (Q2051565) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- An efficient subsumption test pipeline for BS(LRA) clauses (Q2104505) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Making theory reasoning simpler (Q2233504) (← links)
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories (Q2234101) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- Model completeness, covers and superposition (Q2305411) (← links)
- On invariant synthesis for parametric systems (Q2305429) (← links)
- A complete and terminating approach to linear integer solving (Q2307624) (← links)
- Modular proof systems for partial functions with Evans equality (Q2432764) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- On First-Order Model-Based Reasoning (Q2945706) (← links)
- Superposition Modulo Non-linear Arithmetic (Q3172887) (← links)
- Beagle – A Hierarchic Superposition Theorem Prover (Q3454107) (← links)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties (Q3498479) (← links)
- Superposition Modulo Linear Arithmetic SUP(LA) (Q3655193) (← 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)
- First-Order Resolution Methods for Modal Logics (Q4916086) (← links)
- Buchberger's algorithm: A constraint-based completion procedure (Q5096314) (← links)
- Model Evolution with Equality Modulo Built-in Theories (Q5200017) (← links)
- A comprehensive framework for saturation theorem proving (Q5918558) (← links)
- A comprehensive framework for saturation theorem proving (Q5970776) (← links)