scientific article
From MaRDI portal
Publication:2751379
zbMath1011.68129MaRDI QIDQ2751379
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, Automated Reasoning Building Blocks, Alternating two-way AC-tree automata, Automatic Proof and Disproof in Isabelle/HOL, Simplifying proofs in Fitch-style natural deduction systems, Attacking group protocols by refuting incorrect inductive conjectures, Deciding Boolean algebra with Presburger arithmetic, Things to know when implementing KBO, Supporting the formal verification of mathematical texts, Case splitting in an automatic theorem prover for real-valued special functions, Superposition-based equality handling for analytic tableaux, Unifying splitting, Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Hyperresolution for guarded formulae, NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment, First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation, Proofs and Reconstructions, On the verification of security-aware E-services, Automation for interactive proof: first prototype, Superposition decides the first-order logic fragment over ground theories, Semantically-guided goal-sensitive reasoning: inference system and completeness, Encoding Monomorphic and Polymorphic Types, First-order automated reasoning with theories: when deduction modulo theory meets practice, Deciding expressive description logics in the framework of resolution, Superposition for Fixed Domains, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance, Consequence-based and fixed-parameter tractable reasoning in description logics, Translating higher-order clauses to first-order clauses, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Superposition for Bounded Domains, Citius altius fortius, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, MPTP-motivation, implementation, first experiments, On the Saturation of YAGO, SCL(EQ): SCL for first-order logic with equality, Decidability Results for Saturation-Based Model Building, From LCF to Isabelle/HOL, Extending Sledgehammer with SMT Solvers, Formalizing Bachmair and Ganzinger's ordered resolution prover, Using First-Order Theorem Provers in the Jahob Data Structure Verification System, Lightweight relevance filtering for machine-generated resolution problems, A comprehensive framework for saturation theorem proving, Blocking and other enhancements for bottom-up model generation methods, Selecting the Selection, Efficient local reductions to basic modal logic, A unifying splitting framework, Old or heavy? Decaying gracefully with age/weight shapes, Induction in saturation-based proof search, Unsorted Functional Translations, Deciding the Inductive Validity of ∀ ∃ * Queries, Labelled splitting, Superposition Modulo Linear Arithmetic SUP(LA), Subsumption demodulation in first-order theorem proving, A comprehensive framework for saturation theorem proving, A posthumous contribution by Larry Wos: excerpts from an unpublished column, Local is best: efficient reductions to modal logic \textsf{K}, SCL(EQ): SCL for first-order logic with equality, Local reductions for the modal cube, Presenting and Explaining Mizar, Extending Sledgehammer with SMT solvers
