scientific article; zbMATH DE number 3568056
From MaRDI portal
Publication:4139711
zbMath0364.68082MaRDI QIDQ4139711
Publication date: 1978
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
A resolution principle for constrained logics, TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic, Semi-intelligible Isar proofs from machine-generated proofs, 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, SATCHMORE: SATCHMO with RElevancy, Subsumption and implication, A new algorithm for the propositional satisfiability problem, Link inheritance in abstract clause graphs, Negation as failure: careful closure procedure, A structure-preserving clause form translation, Hierarchical deduction, Embedding complex decision procedures inside an interactive theorem prover., Resolution vs. cutting plane solution of inference problems: Some computational experience, Some results and experiments in programming techniques for propositional logic, Branch-and-cut solution of inference problems in propositional logic, Solving propositional satisfiability problems, A parallel approach for theorem proving in propositional logic, History and basic features of the critical-pair/completion procedure, About the Paterson-Wegman linear unification algorithm, Man-machine theorem proving in graph theory, A practically efficient and almost linear unification algorithm, Branching rules for satisfiability, A note on assumptions about Skolem functions, Representing and building models for decidable subclasses of equational clausal logic, Generalized subsumption and its applications to induction and redundancy, Some techniques for proving termination of the hyperresolution calculus, Implication of clauses is undecidable, A Prolog technology theorem prover: Implementation by an extended Prolog compiler, A weight-balanced branching rule for SAT, A note on the completeness of resolution without self-resolution, Efficient solution of linear diophantine equations, A hierarchy of propositional Horn formuls, Hierarchies of polynomially solvable satisfiability problems, Unification theory, Linear and unit-resulting refutations for Horn theories, Defining answer classes using resolution refutation, Near-Horn Prolog and the ancestry family of procedures, Avoiding duplicate proofs with the foothold refinement, Logic applied to integer programming and integer programming applied to logic, 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, An extension to linear resolution with selection function, Strategies for modal resolution: Results and problems, The \(Multi\)-SAT algorithm, A utility-valued logic for decision making, A Noetherian and confluent rewrite system for idempotent semigroups, A simplified problem reduction format, \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE, Connection tableaux with lazy paramodulation, Semantics of Horn and disjunctive logic programs, An efficient solver for weighted Max-SAT, Knowledge-based proof planning, Meta-resolution: An algorithmic formalisation, 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, Removing redundancy from a clause, 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, Parsing as non-Horn deduction, Verifying local stratifiability of logic programs and databases, Producing and verifying extremely large propositional refutations, Linearity and regularity with negation normal form, Unification in a combination of arbitrary disjoint equational theories, Recursive query processing: The power of logic, A complete adaptive algorithm for propositional satisfiability, Compiling a default reasoning system into Prolog, Local simplification, Term rewriting: Some experimental results, Using forcing to prove completeness of resolution and paramodulation, Theorem-proving with resolution and superposition, Theorem proving by chain resolution, Prolog technology for default reasoning: proof theory and compilation techniques, Learning action models from plan examples using weighted MAX-SAT, Linear programs for constraint satisfaction problems, How good are branching rules in DPLL?, A comparative study of several proof procedures, An implementation of Kripke-Kleene semantics, Linear strategy for Boolean ring based theorem proving, Modeling production rules by means of predicate transition networks, The achievement of knowledge bases by cycle search., Closures and fairness in the semantics of programming logic, The approximation of implicates and explanations, Tractable reasoning via approximation, A superposition oriented theorem prover, Backtracking tactics in the backtrack method for SAT, Gentzen-type systems, resolution and tableaux, A relevance restriction strategy for automated deduction, On the mechanical derivation of loop invariants, On preprocessing techniques and their impact on propositional model counting, Goal directed strategies for paramodulation, Unnamed Item, Uniform and non uniform strategies for tableaux calculi for modal logics, Answering atomic queries in indefinite deductive databases, Craig interpolation with clausal first-order tableaux, Propositional calculus problems in CHIP, Simplifying clausal satisfiability problems, Book review of: S. Russell and P. Norvig, Artificial intelligence: a modern approach, Embedding circumscriptive theories in general disjunctive programs, ABox abduction in the description logic \(\mathcal{ALC}\), Subsumption-linear Q-resolution for QBF theorem proving, Subgoal alternation in model elimination, Simplifying and generalizing formulae in tableaux. Pruning the search space and building models, An algorithm for the retrieval of unifiers from discrimination trees, The practicality of generating semantic trees for proofs of unsatisfiability, First order LUB approximations: characterization and algorithms, Partition-based logical reasoning for first-order and propositional theories, Generalized Conflict-Clause Strengthening for Satisfiability Solvers, Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification, SiCoTHEO: Simple competitive parallel theorem provers, XRay: A prolog technology theorem prover for default reasoning: A system description, A new method for knowledge compilation: The achievement by cycle search, Semantic trees revisited: Some new completeness results, An automatic proof of Gödel's incompleteness theorem, A Resolution-based Model Building Algorithm for a Fragment of OCC1N =, 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, 1998–99 Annual Meeting of the Association for Symbolic Logic, Building Theorem Provers, A general framework to build contextual cover set induction provers, Exact Max-SAT solvers for over-constrained problems, Mode-Directed Inverse Entailment for Full Clausal Theories, The search efficiency of theorem proving strategies, The applicability of logic program analysis and transformation to theorem proving, Semantic tableaux with ordering restrictions, Local simplification, Automatic verification of cryptographic protocols with SETHEO, Lemma matching for a PTTP-based top-down theorem prover, Exact knowledge compilation in predicate calculus: The partial achievement case, A classification of non-liftable orders for resolution, Building proofs or counterexamples by analogy in a resolution framework, What you always wanted to know about rigid E-unification, Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions, Combining Instance Generation and Resolution, Set of support, demodulation, paramodulation: a historical perspective, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
