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
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, 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, VAMPIRE, 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
