The following pages link to (Q3743300):
Displaying 50 items.
- Evidence algorithm and inference search in first-order logics (Q286802) (← links)
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- \textbf{R}-calculus without the cut rule (Q351018) (← links)
- Maximal contractions in Boolean algebras (Q362282) (← links)
- An algorithm to compute maximal contractions for Horn clauses (Q543196) (← links)
- Unification in a combination of arbitrary disjoint equational theories (Q582270) (← links)
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness (Q582891) (← links)
- Extracting the resolution algorithm from a completeness proof for the propositional calculus (Q636273) (← links)
- 3-SAT = SAT for a class of normal modal logics (Q673009) (← links)
- R-calculus for ELP: An operational approach to knowledge base maintenance (Q676851) (← links)
- Parsing as non-Horn deduction (Q688151) (← links)
- The \(\lambda \)-calculus and the unity of structural proof theory (Q733755) (← links)
- Negation in rule-based database languages: A survey (Q753476) (← links)
- Negation by default and unstratifiable logic programs (Q753501) (← links)
- Using forcing to prove completeness of resolution and paramodulation (Q757093) (← links)
- Optimizing the clausal normal form transformation (Q809622) (← links)
- Order-sorted logic programming with predicate hierarchy (Q814621) (← links)
- On process equivalence = equation solving in CCS (Q839034) (← links)
- NP-containment for the coherence test of assessments of conditional probability: a fuzzy logical approach (Q877263) (← links)
- Rigid E-unification: NP-completeness and applications to equational matings (Q921913) (← links)
- A semantic approach to interpolation (Q1006639) (← links)
- The RISC ProofNavigator: a proving assistant for program verification in the classroom (Q1019024) (← links)
- Quantified coalition logic (Q1024128) (← links)
- \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver (Q1037644) (← links)
- Resolution on formula-trees (Q1098648) (← links)
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations (Q1100933) (← links)
- The power of temporal proofs (Q1118578) (← links)
- Unsolvable systems of equations and proof complexity (Q1126839) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- Fuzzy term-rewriting system (Q1182011) (← links)
- A semantic backward chaining proof system (Q1193483) (← links)
- A method for simultaneous search for refutations and models by equational constraint solving (Q1198235) (← links)
- Existential instantiation and normalization in sequent natural deduction (Q1198828) (← links)
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi (Q1208732) (← links)
- A key to fuzzy-logic inference (Q1209538) (← links)
- A new method for undecidability proofs of first order theories (Q1209623) (← links)
- Partial logics reconsidered: A conservative approach (Q1261311) (← links)
- Complete sets of transformations for general E-unification (Q1262754) (← links)
- Representing scope in intuitionistic deductions (Q1274448) (← links)
- Gentzen-type systems, resolution and tableaux (Q1311413) (← links)
- Unique complements and decompositions of database schemata (Q1318468) (← links)
- A resolution principle for constrained logics (Q1327159) (← links)
- Proof rules for recursive procedures (Q1329196) (← links)
- A term equality problem equivalent to graph isomorphism (Q1332775) (← links)
- Min-max functions (Q1338772) (← links)
- On proof normalization in linear logic (Q1342248) (← links)
- The saturated tableaux for linear miniscope Horn-like temporal logic (Q1344880) (← links)
- Using automata theory for characterizing the semantics of terminological cycles (Q1380409) (← links)
- Intuitive minimal abduction in sequent calculi (Q1389097) (← links)
- A programmable approach to maintenance of a finite knowledge base (Q1400054) (← links)
