Automated deduction by theory resolution
From MaRDI portal
Publication:1821564
DOI10.1007/BF00244275zbMath0616.68076MaRDI QIDQ1821564
Publication date: 1985
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items
Proof normalization modulo, Connection calculus theorem proving with multiple built-in theories, Theory matrices (for modal logics) using alphabetical monotonicity, The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning, Reduction rules for resolution-based systems, An order-sorted logic for knowledge representation systems, A method for simultaneous search for refutations and models by equational constraint solving, A Prolog technology theorem prover: A new exposition and implementation in Prolog, The ECO family, Exploiting lattices in a theory of space and time, Completing sort hierarchies, A resolution principle for constrained logics, Refutational theorem proving for hierarchic first-order theories, Hybrid reasoning using universal attachment, Hybridizing nonmonotonic inheritance with theorem proving, On Skolemization in constrained logics, Computing answers with model elimination, Theorem proving modulo, Swinging types=functions+relations+transition systems, Constraint solving for proof planning, Efficient algorithms for qualitative reasoning about time, A typed resolution principle for deduction with conditional typing theory, Combination problems for commutative/monoidal theories or how algebra can help in equational unification, Linear and unit-resulting refutations for Horn theories, Structured proof procedures
