Special relations in automated deduction

DOI10.1145/4904.4905zbMath0637.68103OpenAlexW2053547980WikidataQ56288493 ScholiaQ56288493MaRDI QIDQ3777497

Zohar Manna, Richard Waldinger

Publication date: 1986

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/4904.4905

zbMATH Keywords

monotonicitydeduction rulesautomated theorem-provingrelation matchingrelation replacementresolution rules

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Resolution on formula-trees ⋮ Extending resolution to resolution logics ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Unnamed Item ⋮ Rewriting with equivalence relations in ACL2 ⋮ A resolution framework for finitely-valued first-order logics ⋮ Resolution approximation of first-order logics ⋮ The problem of reasoning from inequalities ⋮ An essay on resolution logics ⋮ Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) ⋮ Linearity and regularity with negation normal form ⋮ \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\) ⋮ Deductive synthesis of sorting programs ⋮ Constructing specification morphisms