Lightweight relevance filtering for machine-generated resolution problems
From MaRDI portal
Publication:1006731
DOI10.1016/j.jal.2007.07.004zbMath1183.68560OpenAlexW2013792502WikidataQ57382620 ScholiaQ57382620MaRDI QIDQ1006731
Jia Meng, Lawrence Charles Paulson
Publication date: 25 March 2009
Published in: Journal of Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jal.2007.07.004
Related Items (27)
Improving stateful premise selection with transformers ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ A heuristic prover for real inequalities ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Mining the Archive of Formal Proofs ⋮ System Description: E.T. 0.1 ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Case splitting in an automatic theorem prover for real-valued special functions ⋮ Crystal: Integrating structured queries into a tactic language ⋮ Hammer for Coq: automation for dependent type theory ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Machine Learning for Inductive Theorem Proving ⋮ ATP and presentation service for Mizar formalizations ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Translating higher-order clauses to first-order clauses ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Sledgehammer: Judgement Day ⋮ Premise Selection in the Naproche System ⋮ Machine learning guidance for connection tableaux ⋮ Extending Sledgehammer with SMT Solvers ⋮ Sine Qua Non for Large Theory Reasoning ⋮ Using First-Order Theorem Provers in the Jahob Data Structure Verification System ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Agent-Based HOL Reasoning ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Names are not just sound and smoke: word embeddings for axiom selection ⋮ Extending Sledgehammer with SMT solvers
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A relevance restriction strategy for automated deduction
- The TPTP problem library. CNF release v1. 2. 1
- Automated proof construction in type theory using resolution
- Automation for interactive proof: first prototype
- Automated reasoning. Second international joint conference, IJCAR 2004, Cork, Ireland, July 4--8, 2004. Proceedings.
- Automated Reasoning
- Automated Reasoning
- Automated Reasoning
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
This page was built for publication: Lightweight relevance filtering for machine-generated resolution problems