The following pages link to (Q4139711):
Displaying 50 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Unification in a combination of arbitrary disjoint equational theories (Q582270) (← links)
- A weight-balanced branching rule for SAT (Q597527) (← links)
- Meta-resolution: An algorithmic formalisation (Q671650) (← links)
- Removing redundancy from a clause (Q685346) (← links)
- Parsing as non-Horn deduction (Q688151) (← links)
- Producing and verifying extremely large propositional refutations (Q694550) (← links)
- Linearity and regularity with negation normal form (Q703486) (← links)
- Compiling a default reasoning system into Prolog (Q750134) (← links)
- Term rewriting: Some experimental results (Q757071) (← links)
- Using forcing to prove completeness of resolution and paramodulation (Q757093) (← links)
- Theorem-proving with resolution and superposition (Q757094) (← links)
- Closures and fairness in the semantics of programming logic (Q799098) (← links)
- A relevance restriction strategy for automated deduction (Q814429) (← links)
- Representing and building models for decidable subclasses of equational clausal logic (Q861367) (← links)
- Some techniques for proving termination of the hyperresolution calculus (Q861692) (← links)
- Defining answer classes using resolution refutation (Q881832) (← links)
- Strategies for modal resolution: Results and problems (Q920970) (← links)
- A utility-valued logic for decision making (Q922308) (← links)
- Connection tableaux with lazy paramodulation (Q928656) (← links)
- An efficient solver for weighted Max-SAT (Q933784) (← links)
- Learning action models from plan examples using weighted MAX-SAT (Q1028900) (← links)
- Modeling production rules by means of predicate transition networks (Q1058869) (← links)
- A superposition oriented theorem prover (Q1060857) (← links)
- Subsumption and implication (Q1094152) (← links)
- Link inheritance in abstract clause graphs (Q1097716) (← links)
- Negation as failure: careful closure procedure (Q1097727) (← links)
- A structure-preserving clause form translation (Q1098330) (← links)
- Hierarchical deduction (Q1098332) (← links)
- Resolution vs. cutting plane solution of inference problems: Some computational experience (Q1100093) (← links)
- Some results and experiments in programming techniques for propositional logic (Q1100931) (← links)
- A parallel approach for theorem proving in propositional logic (Q1102766) (← links)
- History and basic features of the critical-pair/completion procedure (Q1103414) (← links)
- About the Paterson-Wegman linear unification algorithm (Q1103417) (← links)
- Man-machine theorem proving in graph theory (Q1104124) (← links)
- A practically efficient and almost linear unification algorithm (Q1105360) (← links)
- Generalized subsumption and its applications to induction and redundancy (Q1110345) (← links)
- Implication of clauses is undecidable (Q1110493) (← links)
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler (Q1114446) (← links)
- A note on the completeness of resolution without self-resolution (Q1119561) (← links)
- Efficient solution of linear diophantine equations (Q1121310) (← links)
- A hierarchy of propositional Horn formuls (Q1122571) (← links)
- Unification theory (Q1124375) (← links)
- Logic applied to integer programming and integer programming applied to logic (Q1130078) (← links)
- An extension to linear resolution with selection function (Q1160497) (← links)
- A Noetherian and confluent rewrite system for idempotent semigroups (Q1168754) (← links)
- A simplified problem reduction format (Q1170894) (← links)
- Semantics of Horn and disjunctive logic programs (Q1177928) (← links)
- Reduction rules for resolution-based systems (Q1187214) (← links)
- An order-sorted logic for knowledge representation systems (Q1193487) (← links)
