The following pages link to (Q3150300):
Displaying 50 items.
- VAMPIRE (Q15455) (← links)
- MaLeS: a framework for automatic tuning of automated theorem provers (Q286787) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Practical solution techniques for first-order MDPs (Q835833) (← links)
- First-order temporal verification in practice (Q851137) (← links)
- Things to know when implementing KBO (Q861708) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- MPTP 0.2: Design, implementation, and initial experiments (Q877826) (← links)
- Combined reasoning by automated cooperation (Q946572) (← links)
- Resolution is cut-free (Q972424) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Solving the \$100 modal logic challenge (Q1006738) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- Stratified resolution (Q1404977) (← links)
- Document models (Q1709112) (← links)
- A navigational logic for reasoning about graph properties (Q1996850) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Introducing \(H\), an institution-based formal specification and verification language (Q2183716) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
- Using relation-algebraic means and tool support for investigating and computing bipartitions (Q2360655) (← links)
- Superposition with equivalence reasoning and delayed clause normal form transformation (Q2486577) (← links)
- Mechanising first-order temporal resolution (Q2486579) (← links)
- Efficient instance retrieval with standard and relational path indexing (Q2486586) (← links)
- From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
- Portfolio theorem proving and prover runtime prediction for geometry (Q2631959) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Theorem proving using clausal resolution: from past to present (Q2695485) (← links)
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (Q2817933) (← links)
- Presenting and Explaining Mizar (Q2867936) (← links)
- An Interactive Derivation Viewer (Q2867942) (← links)
- Unifying Theories of Programming in Isabelle (Q2948230) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- MaLeCoP Machine Learning Connection Prover (Q3010374) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Translating a Dependently-Typed Logic to First-Order Logic (Q3184740) (← links)
- Simulation and Synthesis of Deduction Calculi (Q3185770) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- Playing with AVATAR (Q3454110) (← links)
- Decidable Fragments of Many-Sorted Logic (Q3498453) (← links)
