On a bound for the complexity of terms in the resolution method
From MaRDI portal
Publication:1217465
zbMath0305.68064MaRDI QIDQ1217465
Publication date: 1972
Published in: Proceedings of the Steklov Institute of Mathematics (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Using resolution for deciding solvable classes and building finite models ⋮ One modification of the ordering strategy in the resolution method ⋮ An algorithm for the retrieval of unifiers from discrimination trees ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ Maslov's inverse method and decidable classes ⋮ The search efficiency of theorem proving strategies ⋮ A classification of non-liftable orders for resolution ⋮ Deciding the \(E^+\)-class by an a posteriori, liftable order
This page was built for publication: On a bound for the complexity of terms in the resolution method
