Prolog Technology Reinforcement Learning Prover

DOI10.1007/978-3-030-51054-1_33OpenAlexW3102252921MaRDI QIDQ5049033FDOQ5049033

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

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

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
• On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
• Lemmas: generation, selection, application
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search

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)