Publication:4139711
From MaRDI portal
zbMath0364.68082MaRDI QIDQ4139711
Publication date: 1978
68-02: Research exposition (monographs, survey articles) pertaining to computer science
Related Items
Uniform and non uniform strategies for tableaux calculi for modal logics, 1998–99 Annual Meeting of the Association for Symbolic Logic, An automatic proof of Gödel's incompleteness theorem, Controlled use of clausal lemmas in connection tableau calculi, Connection calculus theorem proving with multiple built-in theories, \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\), Fuzzy logic programming, A general framework to build contextual cover set induction provers, A weight-balanced branching rule for SAT, Meta-resolution: An algorithmic formalisation, Removing redundancy from a clause, Parsing as non-Horn deduction, Linearity and regularity with negation normal form, Logic applied to integer programming and integer programming applied to logic, Semantics of Horn and disjunctive logic programs, Reduction rules for resolution-based systems, An order-sorted logic for knowledge representation systems, Complexity of resolution proofs and function introduction, A method for simultaneous search for refutations and models by equational constraint solving, A new subsumption method in the connection graph proof procedure, Linear resolution for consequence finding, A Prolog technology theorem prover: A new exposition and implementation in Prolog, An efficient algorithm for the 3-satisfiability problem, Verifying local stratifiability of logic programs and databases, Local simplification, Theorem proving by chain resolution, Prolog technology for default reasoning: proof theory and compilation techniques, Linear programs for constraint satisfaction problems, How good are branching rules in DPLL?, An implementation of Kripke-Kleene semantics, The approximation of implicates and explanations, Gentzen-type systems, resolution and tableaux, On the mechanical derivation of loop invariants, A resolution principle for constrained logics, TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic, On subsumption in distributed derivations, Formalizing incomplete knowledge in incomplete databases, Problem solving by searching for models with a theorem prover, Automated deduction with associative-commutative operators, Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, Controlled integration of the cut rule into connection tableau calculi, Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, Embedding complex decision procedures inside an interactive theorem prover., Branch-and-cut solution of inference problems in propositional logic, Solving propositional satisfiability problems, Hierarchies of polynomially solvable satisfiability problems, Extracting models from clause sets saturated under semantic refinements of the resolution rule., Clause trees: A tool for understanding and implementing resolution in automated reasoning, Computing answers with model elimination, Approximating minimal unsatisfiable subformulae by means of adaptive core search, \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE, Linear strategy for Boolean ring based theorem proving, Backtracking tactics in the backtrack method for SAT, A complete adaptive algorithm for propositional satisfiability, The achievement of knowledge bases by cycle search., Tractable reasoning via approximation, SATCHMORE: SATCHMO with RElevancy, A new algorithm for the propositional satisfiability problem, Branching rules for satisfiability, A note on assumptions about Skolem functions, Linear and unit-resulting refutations for Horn theories, Near-Horn Prolog and the ancestry family of procedures, Avoiding duplicate proofs with the foothold refinement, The \(Multi\)-SAT algorithm, Knowledge-based proof planning, Unnamed Item, The practicality of generating semantic trees for proofs of unsatisfiability
