scientific article
From MaRDI portal
Publication:3150300
zbMath1021.68082MaRDI QIDQ3150300
Andrei Voronkov, Alexandre Riazanov
Publication date: 30 September 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (77)
Using relation-algebraic means and tool support for investigating and computing bipartitions ⋮ MaLeS: a framework for automatic tuning of automated theorem provers ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Practical solution techniques for first-order MDPs ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ From informal to formal proofs in Euclidean geometry ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Mining the Archive of Formal Proofs ⋮ Playing with AVATAR ⋮ First-order temporal verification in practice ⋮ Translating a Dependently-Typed Logic to First-Order Logic ⋮ Simulation and Synthesis of Deduction Calculi ⋮ Things to know when implementing KBO ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Introducing \(H\), an institution-based formal specification and verification language ⋮ Unifying Theories of Programming in Isabelle ⋮ Decidable Fragments of Many-Sorted Logic ⋮ An Extension of the Knuth-Bendix Ordering with LPO-Like Properties ⋮ Stratified resolution ⋮ Why3-do: the way of harmonious distributed system proofs ⋮ Recognizing textual entailment and computational semantics ⋮ Model evolution with equality -- revised and implemented ⋮ Theorem proving using clausal resolution: from past to present ⋮ Document models ⋮ Encoding Monomorphic and Polymorphic Types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ SMELS: Satisfiability Modulo Equality with Lazy Superposition ⋮ Resolution-Like Theorem Proving for High-Level Conditions ⋮ LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) ⋮ MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance ⋮ Combined reasoning by automated cooperation ⋮ MaLeCoP Machine Learning Connection Prover ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ A navigational logic for reasoning about graph properties ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ The Relative Power of Semantics and Unification ⋮ An Interactive Driver for Goal-directed Proof Strategies ⋮ Superposition with equivalence reasoning and delayed clause normal form transformation ⋮ Mechanising first-order temporal resolution ⋮ Efficient instance retrieval with standard and relational path indexing ⋮ Resolution is cut-free ⋮ Sledgehammer: Judgement Day ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Interpolation and Symbol Elimination ⋮ Dynamic Reconfiguration via Typed Modalities ⋮ Hammering Floating-Point Arithmetic ⋮ From LCF to Isabelle/HOL ⋮ Extending Sledgehammer with SMT Solvers ⋮ Experimenting with Deduction Modulo ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ On Transfinite Knuth-Bendix Orders ⋮ Lightweight relevance filtering for machine-generated resolution problems ⋮ Solving the \$100 modal logic challenge ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Automated verification of refinement laws ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ A new methodology for developing deduction methods ⋮ Combinations of Theories for Decidable Fragments of First-Order Logic ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Presenting and Explaining Mizar ⋮ An Interactive Derivation Viewer ⋮ Extending Sledgehammer with SMT solvers ⋮ SMELS: satisfiability modulo equality with lazy superposition ⋮ Premise selection for mathematics by corpus analysis and kernel methods ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
Uses Software
This page was built for publication:
