scientific article
From MaRDI portal
Publication:2751377
zbMath0993.68119MaRDI QIDQ2751377
Ullrich Hustadt, Alexander Leitsch, Christian G. Fermüller, Tanel Tammet
Publication date: 21 October 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Semantically-guided goal-sensitive reasoning: model representation, Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications, Simulation and Synthesis of Deduction Calculi, The model evolution calculus as a first-order DPLL method, Representing and building models for decidable subclasses of equational clausal logic, Some techniques for proving termination of the hyperresolution calculus, Tree tuple languages from the logic programming point of view, On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic, Extracting models from clause sets saturated under semantic refinements of the resolution rule., Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Hyperresolution for guarded formulae, Superposition as a decision procedure for timed automata, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Consequence-based and fixed-parameter tractable reasoning in description logics, Canonical Ground Horn Theories, First-Order Resolution Methods for Modal Logics, A Resolution-based Model Building Algorithm for a Fragment of OCC1N =, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, Mechanising first-order temporal resolution, Deciding effectively propositional logic using DPLL and substitution sets, Decidability Results for Saturation-Based Model Building, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics, Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables, Classic-Like Analytic Tableaux for Finite-Valued Logics, Labelled splitting, A new methodology for developing deduction methods, Completeness of hyper-resolution via the semantics of disjunctive logic programs, SGGS decision procedures
