Decision tactics for derivation search in the resolution method

DOI10.1007/BF01093424zbMath0664.03010OpenAlexW2087987601MaRDI QIDQ1115412

N. K. Zamov, V. I. Sharonov

Publication date: 1987

Published in: Journal of Soviet Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01093424

zbMATH Keywords

resolution methoddecidable classderivability of formulasbounded term ranksordering tactics

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

This page was built for publication: Decision tactics for derivation search in the resolution method