Well-behaved inference rules for first-order theorem proving

DOI10.1023/A:1006027228476zbMath0926.03010OpenAlexW1562946501MaRDI QIDQ1272612

Jinzhao Wu, Zhuo-Jun Liu

Publication date: 29 November 1999

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1006027228476

zbMATH Keywords

completenessresolutionBoolean ring based deductionBoolean ring based theorem provingexpansion-oriented strategieslock strategysemantic strategysuperposition inference rules

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

This page was built for publication: Well-behaved inference rules for first-order theorem proving