scientific article
From MaRDI portal
Publication:2751353
zbMath0993.03008MaRDI QIDQ2751353
Leo Bachmair, Harald Ganzinger
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
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 (only showing first 100 items - show all)
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
This page was built for publication:
