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 transformersSemi-intelligible Isar proofs from machine-generated proofsA heuristic prover for real inequalitiesAutomatic Proof and Disproof in Isabelle/HOLMining the Archive of Formal ProofsSystem Description: E.T. 0.1A learning-based fact selector for Isabelle/HOLCase splitting in an automatic theorem prover for real-valued special functionsCrystal: Integrating structured queries into a tactic languageHammer for Coq: automation for dependent type theoryExtensional higher-order paramodulation in Leo-IIIMachine Learning for Inductive Theorem ProvingATP and presentation service for Mizar formalizationsLearning-assisted theorem proving with millions of lemmasTranslating higher-order clauses to first-order clausesTheorem Proving in Large Formal Mathematics as an Emerging AI FieldSledgehammer: Judgement DayPremise Selection in the Naproche SystemMachine learning guidance for connection tableauxExtending Sledgehammer with SMT SolversSine Qua Non for Large Theory ReasoningUsing First-Order Theorem Provers in the Jahob Data Structure Verification SystemPerformance of Clause Selection Heuristics for Saturation-Based Theorem ProvingAgent-Based HOL ReasoningReliable reconstruction of fine-grained proofs in a proof assistantNames are not just sound and smoke: word embeddings for axiom selectionExtending Sledgehammer with SMT solvers


Uses Software


Cites Work




This page was built for publication: Lightweight relevance filtering for machine-generated resolution problems