System Description: E 1.8
From MaRDI portal
Publication:2870167
DOI10.1007/978-3-642-45221-5_49zbMath1407.68442OpenAlexW2583369873MaRDI QIDQ2870167
Publication date: 17 January 2014
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-45221-5_49
Related Items
Deepalgebra -- an outline of a program ⋮ Heterogeneous heuristic optimisation and scheduling for first-order theorem proving ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Fast and slow enigmas and parental guidance ⋮ Implementing Superposition in iProver (System Description) ⋮ Caper ⋮ Mining the Archive of Formal Proofs ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ Towards finding longer proofs ⋮ The role of entropy in guiding a connection prover ⋮ Learning theorem proving components ⋮ History and Prospects for First-Order Automated Deduction ⋮ Quantifier-Free Equational Logic and Prime Implicate Generation ⋮ Cooperating Proof Attempts ⋮ System Description: E.T. 0.1 ⋮ Efficient Low-Level Connection Tableaux ⋮ Ordered Resolution for Coalition Logic ⋮ The Proof Certifier Checkers ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Hammer for Coq: automation for dependent type theory ⋮ Formalization of the resolution calculus for first-order logic ⋮ Introducing \(H\), an institution-based formal specification and verification language ⋮ Unnamed Item ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ On structures of regular standard contradictions in propositional logic ⋮ Targeted configuration of an SMT solver ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Random Forests for Premise Selection ⋮ Lemmatization for Stronger Reasoning in Large Theories ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Relaxed weighted path order in theorem proving ⋮ Relational characterisations of paths ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Machine learning guidance for connection tableaux ⋮ Superposition with lambdas ⋮ Scalable fine-grained proofs for formula processing ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Internal Guidance for Satallax ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ GRUNGE: a grand unified ATP challenge ⋮ Names are not just sound and smoke: word embeddings for axiom selection ⋮ Faster, higher, stronger: E 2.3 ⋮ E Theorem Prover ⋮ Extending Maximal Completion (Invited Talk) ⋮ Formalization of the Resolution Calculus for First-Order Logic ⋮ Complexity of translations from resolution to sequent calculus ⋮ Ground joinability and connectedness in the superposition calculus ⋮ On interpolation in automated theorem proving
Uses Software
