Fetching the paper…
Reading the bibliography…
In this paper, we consider the problem of learning a first-order theorem prover that uses a representation of beliefs in mathematical claims to construct proofs.
The Continuum of Inductive Methods
Rudolf Carnap · 1952
Earlier work this paper cites.
Some Remarks on Infinitely Long Formulas
Leon Henkin · 1961
Earlier work this paper cites.
Concerning Measures in First Order Calculi
Haim Gaifman · 1964
Earlier work this paper cites.
Distributive Normal Forms in First-Order Logic
Jaakko Hintikka · 1965
Earlier work this paper cites.
A Two-Dimensional Continuum of Inductive Methods
Jaakko Hintikka · 1966
Earlier work this paper cites.
Assigning Probabilities to Logical Formulas
Dana Scott and Peter Krauss · 1966
Earlier work this paper cites.
Slightly more realistic personal probability
Ian Hacking · 1967
Earlier work this paper cites.
Surface Information and Depth Information
Jaakko Hintikka · 1970
Earlier work this paper cites.
Towards a General Theory of Auxiliary Concepts and Definability in First-Order Theories
Jaakko Hintikka and Raimo Tuomela · 1970
Earlier work this paper cites.
Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic
Jaakko Hintikka · 1973
Earlier work this paper cites.
AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search
Douglas B. Lenat · 1976
Earlier work this paper cites.
Dialogische Logik
Kuno Lorenz and Paul Lorenzen · 1978
Earlier work this paper cites.
Impossible Possible Worlds Vindicated
Jaakko Hintikka · 1979
Earlier work this paper cites.
Old Evidence and Logical Omniscience in Bayesian Confirmation Theory
Daniel Garber · 1983
Earlier work this paper cites.
Induction of Decision Trees
J. R. Quinlan · 1986
Earlier work this paper cites.
A logical approach to reasoning by analogy
Todd Davies and Stuart Russell · 1987
Earlier work this paper cites.
Modelling Legal Argument: Reasoning with Cases and Hypotheticals
Kevin D. Ashley · 1988
Earlier work this paper cites.
The Average Distance and the Independence Number
Fan R. K. Chung · 1988
Earlier work this paper cites.
On Conjectures of Graffiti
Siemion Fajtlowicz · 1988
Earlier work this paper cites.
Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference
Judea Pearl · 1988
Earlier work this paper cites.
Analogy by Similarity
Stuart Russell · 1988
Earlier work this paper cites.
The Logical View of Conditioning and its Application to Possibility and Evidence Theories
Didier Dubois and Henri Prade · 1990
Earlier work this paper cites.
Invention and Exploration in Discovery
Kenneth W. Haase · 1990
Earlier work this paper cites.
On the relationship between abduction and deduction
Luca Console, Daniele Theseider Dupré, and Pietro Torasso · 1991
Earlier work this paper cites.
Practical Issues in Temporal Difference Learning
Gerald Tesauro · 1992
Earlier work this paper cites.
First order abduction via tableau and sequent calculi
Marta Cialdea Mayer and Fiora Pirri · 1993
Earlier work this paper cites.
Formulas of First-Order Logic in Distributive Normal Form
Karen Nelte · 1997
Cited alongside, same era.
Epistemic Logic and Logical Omniscience: A Survey
Kwang Mong Sim · 1997
Cited alongside, same era.
Handbook of Logic in Artificial Intelligence and Logic Programming , volume 5
Dov M. Gabbay, Christopher John Hogger, and John Alan Robinson · 1998
Cited alongside, same era.
The Lengths of Proofs
Pavel Pudlák · 1998
Cited alongside, same era.
Automatic Concept Formation in Pure Mathematics
Simon Colton, Alan Bundy, and Toby Walsh · 1999
Cited alongside, same era.
Game-Theoretical Semantics as a Challenge to Proof Theory
Jaakko Hintikka · 1999
Cited alongside, same era.
Functional Analysis
First-Order Logic and Automated Theorem Proving
Melvin Fitting · 2012
Later among the works it cites.
Machine Learning in Proof General: Interfacing Interfaces, 2012
Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov · 2012
Later among the works it cites.
What kind of uncertainty is that? using personal probability for expressing one’s thinking about logical and mathematical propositions
Teddy Seidenfeld, Mark J. Schervish, and Joseph B. Kadane · 2012
Later among the works it cites.
A Machine-Checked Proof of the Odd Order Theorem
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al · 2013
Later among the works it cites.
Probabilities on Sentences in an Expressive Logic
Marcus Hutter, John W. Lloyd, Kee Siong Ng, and William T.B. Uther · 2013
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
George Bachman and Lawrence Narici · 2000
Cited alongside, same era.
Topology
James R. Munkres · 2000
Cited alongside, same era.
The Automation of Proof by Mathematical Induction
Alan Bundy · 2001
Cited alongside, same era.
Inductionless Induction
Hubert Comon · 2001
Cited alongside, same era.
Elementary Predicate Logic
Wilfrid Hodges · 2001
Cited alongside, same era.
Abduction in Logic Programming
Marc Denecker and Antonis Kakas · 2002
Cited alongside, same era.
Distributed Representations of Words and Phrases and their Compositionality
Tomas Mikolov, Ilya Sutskever, Kai Chen, Greg S. Corrado, and Jeff Dean · 2013
Later among the works it cites.
The Algorithmic Mind: A Study of Inference in Action
Thomas F. Icard III · 2014
Later among the works it cites.
Machine learning of Coq proof guidance: First experiments, 2014
Cezary Kaliszyk, Lionel Mamane, and Josef Urban · 2014
Later among the works it cites.
Is it plausible?
Barry Mazur · 2014
Later among the works it cites.
Logic in Games
Johan van Benthem · 2014
Later among the works it cites.
Scott Garrabrant, Tsvi Benson-Tilsen, Andrew Critch, Nate Soares, and Jessica Taylor · 2016
Later among the works it cites.
Deepmath-deep sequence models for premise selection
Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Een, Francois Chollet, and Josef Urban · 2016
Later among the works it cites.
Mastering the game of Go with deep neural networks and tree search
David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al · 2016
Later among the works it cites.
A fully automatic theorem prover with human-style output
Mohan Ganesalingam and William Timothy Gowers · 2017
Later among the works it cites.
TacticToe: Learning to reason with HOL4 Tactics
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban · 2017
Later among the works it cites.
Holstep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Later among the works it cites.
Deep Network Guided Proof Search
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Later among the works it cites.
Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm, 2017
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al · 2017
Later among the works it cites.
A Dynamic Solution to the Problem of Logical Omniscience
Jens Christian Bjerring and Mattias Skipper · 2018
Later among the works it cites.
Gamepad: A Learning Environment for Theorem Proving, 2018
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever · 2018
Later among the works it cites.
Reinforcement Learning of Theorem Proving, 2018
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Mirek Olšák · 2018
Later among the works it cites.
Learning a SAT Solver from Single-Bit Supervision, 2018
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill · 2018
Later among the works it cites.
Manuscript 514
Peirce Charles Sanders · 2019
Closest in time.
Coq, accessed 2019-3-31
Coq · 2019
Closest in time.
Isabelle, accessed 2019-3-31
Isabelle · 2019
Closest in time.
Mizar, accessed 2019-4-6
Mizar · 2019
Closest in time.