Graph sequence learning for premise selection

DOI10.1016/J.JSC.2024.102376MaRDI QIDQ6650565zbMATH OpenFDO

Authors Edvard K. Holden, Konstantin Korovin

Publication date 9 December 2024

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JSC.2024.102376

zbMATH Keywords

automated theorem provinggraph neural networkmachine learningpremise selectionsequence learning

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Artificial neural networks and deep learning (68T07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Improving stateful premise selection with transformers
• Premise selection for mathematics by corpus analysis and kernel methods
• Premise selection in the Naproche system
• Overview and evaluation of premise selection techniques for large theory mathematics

Cites work

• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• ATP and presentation service for Mizar formalizations
• ATPboost: learning premise selection in binary setting with ATP feedback
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Fast and slow enigmas and parental guidance
• Framing image description as a ranking task: data, models and evaluation metrics
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• scientific article; zbMATH DE number 1670746 (Why is no real title available?)
• Implementing Superposition in iProver (System Description)
• Improving stateful premise selection with transformers
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Isabelle/HOL. A proof assistant for higher-order logic
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Lightweight relevance filtering for machine-generated resolution problems
• Machine learning guidance for connection tableaux
• MaSh: machine learning for Sledgehammer
• MizAR 40 for Mizar 40
• MPTP 0.2: Design, implementation, and initial experiments
• Multidimensional binary search trees used for associative searching
• Neural precedence recommender
• Premise selection for mathematics by corpus analysis and kernel methods
• Property invariant embedding for automated reasoning
• Random forests for premise selection
• Sine qua non for large theory reasoning
• System description: E 1.8
• Targeted configuration of an SMT solver
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• The role of the Mizar mathematical library for interactive proof development in Mizar
• The Structure and Function of Complex Networks

Cited in

(1)

• ATWGNNS: graph simplified representation and learning of logical formula for premise selection

This page was built for publication: Graph sequence learning for premise selection

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6650565)