E Theorem Prover
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Using the TPTP Language for Writing Derivations and Finite Interpretations
- Hammering towards QED
- Computing finite models by reduction to function-free clause logic
- An interactive derivation viewer
- Proof simplification and automated theorem proving
- First-order resolution methods for modal logics
- Selecting the selection
- The TPTP typed first-order form with arithmetic
- checkbashisms
- Theory and Applications of Relational Structures as Knowledge Instruments
- NeuroSAT
- Towards a unified ordering for superposition-based automated reasoning
- Combining induction and saturation-based theorem proving
- Premise selection in the Naproche system
- A formally verified interpreter for a shell-like programming language
- Fast and slow enigmas and parental guidance
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- scientific article; zbMATH DE number 5295699 (Why is no real title available?)
- Formal mathematics on display: a wiki for Flyspeck
- Efficient encodings of first-order Horn formulas in equational logic
- From LCF to Isabelle/HOL
- Encoding monomorphic and polymorphic types
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- Coming to terms with quantified reasoning
- Superposition with first-class booleans and inprocessing clausification
- Automated Reasoning About Metric and Topology
- qbf2epr
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- Automated Reasoning
- Portfolio theorem proving and prover runtime prediction for geometry
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Automated theorem proving in quasigroup and loop theory
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Induction in saturation-based proof search
- Names are not just sound and smoke: word embeddings for axiom selection
- Relational characterisations of paths
- Ground joinability and connectedness in the superposition calculus
- Things to know when implementing KBO
- System description: E.T. 0.1
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- PyRes
- A comprehensive framework for saturation theorem proving
- Making higher-order superposition work
- Superposition with lambdas
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- An assumption-based approach for solving the minimal S5-satisfiability problem
- A generic framework for implicate generation modulo theories
- Superposition for \(\lambda\)-free higher-order logic
- Scalable fine-grained proofs for formula processing
- Superposition with lambdas
- lazyCoP
- CoLiS
- Shellcheck
- MedleySolver
- Nunchaku
- From search to computation: redundancy criteria and simplification at work
- A principle for incorporating axioms into the first-order translation of modal formulae.
- Local is best: efficient reductions to modal logic \textsf{K}
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- The TPTP World -- infrastructure for automated reasoning
- SOLAR: An automated deduction system for consequence finding
- MaLeCoP. Machine learning connection prover
- MPTP-motivation, implementation, first experiments
- Automatic proof and disproof in Isabelle/HOL
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- Model evolution with equality -- revised and implemented
- MizAR 40 for Mizar 40
- Aligator
- ILTP
- LEO-II
- Nitpick
- QOCA
- SOLAR
- TPS
- Hilberticus
- Isabelle/HOL
- RuleML
- MizarMode
- AFRA
- ToolBus
- MPTP
- MPTP 0.2
- OTTER
- VAMPIRE
- Paradox
- THF0
- Darwin
- SMT-LIB
- SPASS
- TPTP
- Isar
- MoMM
- Mizar
- cvc3
- SPASS+T
This page was built for software: E Theorem Prover
