scientific article; zbMATH DE number 1037485
From MaRDI portal
Publication:4345253
zbMath0881.68106MaRDI QIDQ4345253
Yunshan Zhu, David Alan Plaisted
Publication date: 22 July 1997
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
term rewritingresolution calculusmodel eliminationclause linkingrefutational (automated) theorem provingsearch space complexity
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (10)
Semantically-guided goal-sensitive reasoning: model representation ⋮ History and Prospects for First-Order Automated Deduction ⋮ On First-Order Model-Based Reasoning ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Resolution remains hard under equivalence ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Theory decision by decomposition ⋮ SGGS decision procedures ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective
Uses Software
This page was built for publication:
