scientific article

Publication date: 27 August 2002

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

survey resolution-based theorem proving resolution refinements resolution strategies

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items

A first polynomial non-clausal class in many-valued logic, Unifying splitting, Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments, Superposition for higher-order logic, Lemmaless induction in trace logic, Unified decomposition-aggregation (UDA) rules: dynamic, schematic, novel axioms, Formalizing Bachmair and Ganzinger's ordered resolution prover, Superposition with lambdas, A comprehensive framework for saturation theorem proving, A comprehensive framework for saturation theorem proving, Extracting unsatisfiable cores for LTL via temporal resolution, Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies, Semi-intelligible Isar proofs from machine-generated proofs, Vampire with a brain is a good ITP hammer, Automated Reasoning Building Blocks, Alternating two-way AC-tree automata, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, Cooperating Proof Attempts, Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations, Ordered Resolution for Coalition Logic, Binary resolution over Boolean lattices, The model evolution calculus as a first-order DPLL method, A clausal resolution method for branching-time logic \(\text{ECTL}^+\), Case splitting in an automatic theorem prover for real-valued special functions, A verified SAT solver framework with learn, forget, restart, and incrementality, Superposition-based equality handling for analytic tableaux, Unnamed Item, Extending a Resolution Prover for Inequalities on Elementary Functions, The Ackermann approach for modal logic, correspondence theory and second-order reduction, Stratified resolution, Hyperresolution for guarded formulae, Resolution with order and selection for hybrid logics, ABox abduction in the description logic \(\mathcal{ALC}\), NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment, Unnamed Item, Superposition as a decision procedure for timed automata, Reliability of mathematical inference, Theorem proving using clausal resolution: from past to present, First-order automated reasoning with theories: when deduction modulo theory meets practice, Limits of theory sequences over algebraically closed fields and applications., Deciding expressive description logics in the framework of resolution, On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas, SMELS: Satisfiability Modulo Equality with Lazy Superposition, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., Engineering DPLL(T) + Saturation, Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators, Reasoning on UML class diagrams, Consequence-based and fixed-parameter tractable reasoning in description logics, Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \), Mechanically certifying formula-based Noetherian induction reasoning, Enhancing unsatisfiable cores for LTL with information on temporal relevance, A resolution calculus for the branching-time temporal logic CTL, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, The Blossom of Finite Semantic Trees, From Search to Computation: Redundancy Criteria and Simplification at Work, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Constructing Bachmair-Ganzinger Models, Planning with Effectively Propositional Logic, First-Order Resolution Methods for Modal Logics, Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01)., Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, Superposition with equivalence reasoning and delayed clause normal form transformation, Mechanising first-order temporal resolution, MetiTarski: An automatic theorem prover for real-valued special functions, Linearity and regularity with negation normal form, Tractable query answering and rewriting under description logic constraints, Abstract canonical presentations, Interpolation and Symbol Elimination, A Refined Resolution Calculus for CTL, Fair Derivations in Monodic Temporal Reasoning, Decidability Results for Saturation-Based Model Building, Optimized Query Rewriting for OWL 2 QL, On Bridging Simulation and Formal Verification, Lightweight relevance filtering for machine-generated resolution problems, Decision Procedures for Automating Termination Proofs, Unnamed Item, Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables, Blocking and other enhancements for bottom-up model generation methods, Combining induction and saturation-based theorem proving, Selecting the Selection, Predicate Elimination for Preprocessing in First-Order Theorem Proving, Lifting QBF Resolution Calculi to DQBF, A unifying splitting framework, Superposition with first-class booleans and inprocessing clausification, Confidences for commonsense reasoning, Neural precedence recommender, Improving ENIGMA-style clause selection while learning from history, GKC: a reasoning system for large knowledge bases, Boundary Points and Resolution, Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations, Labelled splitting, A new methodology for developing deduction methods, Combining Instance Generation and Resolution, Reinterpreting dependency schemes: soundness meets incompleteness in DQBF, Completeness of hyper-resolution via the semantics of disjunctive logic programs, Deciding \(\mathcal H_1\) by resolution, Rewriting Conjunctive Queries over Description Logic Knowledge Bases, MetiTarski: An Automatic Prover for the Elementary Functions, Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif, Subsumption demodulation in first-order theorem proving, Layered clause selection for theory reasoning (short paper), Set of support, demodulation, paramodulation: a historical perspective, An efficient subsumption test pipeline for BS(LRA) clauses, Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL, Semantic relevance, GK: implementing full first order default logic for commonsense reasoning (system description), The possibilistic Horn non-clausal knowledge bases, SMELS: satisfiability modulo equality with lazy superposition, The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies, SAT-Inspired Eliminations for Superposition

Uses Software

Ordered_Resolution_Prover