A study of continuous vector representations for theorem proving

DOI10.1093/LOGCOM/EXAB006MaRDI QIDQ5019287zbMATH OpenOpenAlexWikidataFDO

Authors Stanisław Purgał, Julian Parsert, Cezary Kaliszyk

Publication date 3 January 2022

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2101.09142

zbMATH Keywords

autoencodingMizarpremise selectiontheorem proving

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX) Computer science (68-XX)

Recommendations

• Property invariant embedding for automated reasoning
• Towards the automatic mathematician
• Searching for mathematical formulas based on graph representation learning
• Theorem proving in large formal mathematics as an emerging AI field
• Premise selection for mathematics by corpus analysis and kernel methods

Cited in

(3)

• \texttt{gym-saturation}: gymnasium environments for saturation provers (system description)
• Learning guided automated reasoning: a brief survey
• ATWGNNS: graph simplified representation and learning of logical formula for premise selection

This page was built for publication: A study of continuous vector representations for theorem proving

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