scientific article; zbMATH DE number 1037485
From MaRDI portal
Publication:4345253
zbMATH Open0881.68106MaRDI QIDQ4345253FDOQ4345253
Authors: Yunshan Zhu, David A. Plaisted 
Publication date: 22 July 1997
Title of this publication is not available (Why is that?)
Recommendations
term rewritingresolution calculusmodel eliminationclause linkingrefutational (automated) theorem provingsearch space complexity
Cited In (21)
- Title not available (Why is that?)
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Title not available (Why is that?)
- Title not available (Why is that?)
- The search efficiency of theorem proving strategies
- Semantically-guided goal-sensitive reasoning: model representation
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Shortening of proof length is elusive for theorem provers
- Eliminating dublication with the hyper-linking strategy
- Theory decision by decomposition
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- On First-Order Model-Based Reasoning
- Limited resource strategy in resolution theorem proving
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Title not available (Why is that?)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- History and prospects for first-order automated deduction
- Resolution remains hard under equivalence
- A relevance restriction strategy for automated deduction
- SGGS decision procedures
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4345253)
