The following pages link to Resolution theorem proving (Q2751353):
Displaying 28 items.
- First-Order Resolution Methods for Modal Logics (Q4916086) (← links)
- Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01). (Q4916226) (← links)
- (Q4989394) (← links)
- Linking focusing and resolution with selection (Q5005105) (← links)
- (Q5111307) (← links)
- Interpolation and Symbol Elimination (Q5191103) (← links)
- A Refined Resolution Calculus for CTL (Q5191106) (← links)
- Fair Derivations in Monodic Temporal Reasoning (Q5191107) (← links)
- Decidability Results for Saturation-Based Model Building (Q5191116) (← links)
- Optimized Query Rewriting for OWL 2 QL (Q5200025) (← links)
- Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif (Q5253587) (← links)
- A resolution calculus for the branching-time temporal logic CTL (Q5410337) (← links)
- On Bridging Simulation and Formal Verification (Q5452712) (← links)
- Rewriting Conjunctive Queries over Description Logic Knowledge Bases (Q5504588) (← links)
- MetiTarski: An Automatic Prover for the Elementary Functions (Q5505501) (← links)
- SAT-Inspired Eliminations for Superposition (Q5875949) (← links)
- Superposition with lambdas (Q5918381) (← links)
- A comprehensive framework for saturation theorem proving (Q5918558) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5919011) (← links)
- A comprehensive framework for saturation theorem proving (Q5970776) (← links)
- A first polynomial non-clausal class in many-valued logic (Q6083144) (← links)
- Unifying splitting (Q6103590) (← links)
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments (Q6149592) (← links)
- Superposition for higher-order logic (Q6156638) (← links)
- Lemmaless induction in trace logic (Q6160563) (← links)
- ALASCA: reasoning in quantified linear arithmetic (Q6535381) (← links)
- Lemmas: generation, selection, application (Q6541149) (← links)
- First order Büchi automata and their application to verification of LTL specifications (Q6643476) (← links)
