Lightweight relevance filtering for machine-generated resolution problems

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

zbMATH Keywords

automated reasoninginteractive theorem provingrelevance filteringproving in large theories

Mathematics Subject Classification ID

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

• VAMPIRE
• TPTP
• E Theorem Prover

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