Completely non-clausal theorem proving
From MaRDI portal
Publication:1157923
DOI10.1016/0004-3702(82)90011-XzbMath0472.68053WikidataQ56515254 ScholiaQ56515254MaRDI QIDQ1157923
Publication date: 1982
Published in: Artificial Intelligence (Search for Journal in Brave)
Related Items
Generalized resolution and NC-resolution, A structure-preserving clause form translation, Resolution on formula-trees, Embedding complex decision procedures inside an interactive theorem prover., Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system, Filter-based resolution principle for lattice-valued propositional logic LP\((X)\), Extending resolution to resolution logics, Weighting strategy for non-clausal resolution, A first polynomial non-clausal class in many-valued logic, Comparisons Among α-Generalized Resolution Methods in $$\fancyscript{L}_{n \times 2}$$F(X), Exploiting data dependencies in many-valued logics, An epistemic model of logic programming, Automatic theorem proving. II, A resolution framework for finitely-valued first-order logics, Resolution approximation of first-order logics, An essay on resolution logics, Superposition with equivalence reasoning and delayed clause normal form transformation, 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)\), \(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\), Making higher-order superposition work, Making higher-order superposition work, On Theorem Proving in Annotated Logics, Superposition with first-class booleans and inprocessing clausification, Synthetic programming, Deductive synthesis of sorting programs, Linear strategy for Boolean ring based theorem proving, Synthetic tableaux: Minimal tableau search heuristics, The possibilistic Horn non-clausal knowledge bases, A resolution rule for well-formed formulae
Cites Work
