Pages that link to "Item:Q1157923"
From MaRDI portal
The following pages link to Completely non-clausal theorem proving (Q1157923):
Displayed 31 items.
- Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) (Q545319) (← links)
- An essay on resolution logics (Q687163) (← links)
- Linearity and regularity with negation normal form (Q703486) (← links)
- Synthetic programming (Q761788) (← links)
- A resolution rule for well-formed formulae (Q808295) (← links)
- Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) (Q867665) (← links)
- An epistemic model of logic programming (Q918192) (← links)
- A structure-preserving clause form translation (Q1098330) (← links)
- Resolution on formula-trees (Q1098648) (← links)
- A resolution framework for finitely-valued first-order logics (Q1185455) (← links)
- Resolution approximation of first-order logics (Q1187026) (← links)
- Generalized resolution and NC-resolution (Q1331227) (← links)
- Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) (← links)
- Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system (Q1364068) (← links)
- Linear strategy for Boolean ring based theorem proving (Q1579733) (← links)
- Deductive synthesis of sorting programs (Q1822927) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
- Synthetic tableaux: Minimal tableau search heuristics (Q2104533) (← links)
- The possibilistic Horn non-clausal knowledge bases (Q2105624) (← links)
- Superposition with equivalence reasoning and delayed clause normal form transformation (Q2486577) (← links)
- Comparisons Among α-Generalized Resolution Methods in $$\fancyscript{L}_{n \times 2}$$F(X) (Q2963698) (← links)
- Extending resolution to resolution logics (Q3211281) (← links)
- Weighting strategy for non-clausal resolution (Q3499018) (← links)
- Automatic theorem proving. II (Q3793764) (← links)
- On Theorem Proving in Annotated Logics (Q4443407) (← links)
- Exploiting data dependencies in many-valued logics (Q4868234) (← links)
- Making higher-order superposition work (Q5918403) (← links)
- Making higher-order superposition work (Q5918575) (← links)
- \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\) (Q5946276) (← links)
- \(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\) (Q5946327) (← links)
- A first polynomial non-clausal class in many-valued logic (Q6083144) (← links)