Investigations into Proof Structures
We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to {\L}ukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of {\L}ukasiewicz's problem was automatically discovered that is much shorter than any proof found before by man or machine.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs w…
LEMMAMathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs
Large language models (LLMs) can solve arithmetic word problems with high accuracy, but little is known about how well they generalize to problems that are more complex than the ones on which they have been trained. Empi…
In-Context LearningDetecting Argumentative Discourse Acts with Linguistic Alignment
We report the results of preliminary investigations into the relationship between linguistic alignment and dialogical argumentation at the level of discourse acts. We annotated a proof of concept dataset with illocutions…
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving
Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinato…
Automated Theorem ProvingLearning Algebraic Structures: Preliminary Investigations
We employ techniques of machine-learning, exemplified by support vector machines and neural classifiers, to initiate the study of whether AI can "learn" algebraic structures. Using finite groups and finite rings as a con…
BIG-bench Machine Learning