Prolog Technology Reinforcement Learning Prover

DOI10.1007/978-3-030-51054-1_33MaRDI QIDQ5049033zbMATH OpenOpenAlexFDO

Authors Zsolt Zombori, Josef Urban, Chad E. Brown

Publication date 9 November 2022

Published in Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

reinforcement learningautomated theorem provinglogic programmingconnection tableau calculus

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Deep network guided proof search
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ENIGMA: efficient learning-based inference guiding machine
• ENIGMAWatch: ProofWatch meets ENIGMA
• Efficient description logic reasoning in Prolog: The DLog system
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• IeanCOP: lean connection-based theorem proving
• Inductive Logic Programming: Theory and methods
• MPTP 0.2: Design, implementation, and initial experiments
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• MaLeCoP. Machine learning connection prover
• MizAR 40 for Mizar 40
• MleanCoP: a connection prover for first-order modal logic
• Model elimination and connection tableau procedures
• On connections and higher-order logic
• Premise selection for mathematics by corpus analysis and kernel methods
• Reinforcement learning. An introduction
• SWI-Prolog
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• lean\(T^ AP\): Lean tableau-based deduction

Cited in

(7)

• Eliminating models during model elimination
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• The role of entropy in guiding a connection prover
• Towards finding longer proofs
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
• Lemmas: generation, selection, application

Describes a project that uses

Uses Software

• MPTP 0.2
• VAMPIRE
• PicoSAT
• MaLeCoP
• leanCoP
• ileanCoP
• DLog
• leanTAP
• E Theorem Prover
• MaLARea
• SWI-Prolog
• XGBoost
• FEMaLeCoP
• MleanCoP
• ENIGMA
• GitHub
• HOList

This page was built for publication: Prolog Technology Reinforcement Learning Prover

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