Generating theorems by generating proof structures

Cites work

\(\lambda\) to SKI, semantically -- declarative pearl
A finitely axiomatized formalization of predicate calculus with equality
A legacy recalled and a tradition continued
Applying tree languages in proof theory
Asymptotic enumeration of compacted binary trees of bounded right height
Automated proof compression by invention of new definitions
Automated theorem proving for Metamath
Combinatory logic. With two sections by William Craig.
Conquering the Meredith single axiom
Faster, higher, stronger: E 2.3
From Schütte’s Formal Systems to Modern Automated Deduction
Grammar-Based Tree Compression
scientific article; zbMATH DE number 4209640 (Why is no real title available?)
scientific article; zbMATH DE number 4063061 (Why is no real title available?)
scientific article; zbMATH DE number 3774914 (Why is no real title available?)
scientific article; zbMATH DE number 48763 (Why is no real title available?)
scientific article; zbMATH DE number 1042221 (Why is no real title available?)
scientific article; zbMATH DE number 1470716 (Why is no real title available?)
scientific article; zbMATH DE number 194911 (Why is no real title available?)
Investigations into proof structures
Learning from Łukasiewicz and Meredith: investigations into proof structures
Learning-assisted theorem proving with millions of lemmas
Lemmas: generation, selection, application
Logics and type systems in theory and practice. Essays dedicated to Herman Geuvers on the occasion of his 60th birthday
Principal type-schemes and condensed detachment
Restricting backtracking in connection calculi
SWI-Prolog
The resonance strategy
The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
Witness theory. Notes on -calculus and logic
Über die Bausteine der mathematischen Logik.

This page was built for publication: Generating theorems by generating proof structures

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