Realization of a geometry theorem proving machine

By H. Gelernter. 1995

Subfields: Program Analysis & Verification, Automated Theorem Proving & Formal Methods

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Program Analysis & Verification

In Automated Theorem Proving & Formal Methods

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, background): “Second, mathematical reasoning is in itself a central AI task, its study dating back to at least Gelernter (1959) and Wang (1960) and continuing to today (Lu et al., 2023).”
Why AM and EURISKO Appear to Work (1984, background): “Using bags of T's for numbers is tapping into the same source of power as Gelernter [3] did; namely, the power of having an analogic representation, one in which there is a closeness between the data structures employed and the abstract concept it represents---again, an issue of the relationship bet”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, background): “Mechanising theorem proving has been a grand challenge of artiﬁcial intelligence since the late 1950s [Gelernter, 1959].”
ON THE ANALYSIS OF HUMAN PROBLEM SOLVING PROTOCOLS (1966, methodology): “An example is provided by the program for proving theorems in plane geometry [11], which uses both a space of symbolic expressions, representing theorems, and a space of coordinates, representing the diagram.”
Mental Models in Cognitive Science (1980, background): “Gelemter’s (1963) program for proving geometric theorems, and Funt’s 1977) program for making inferences about the stability of arrangements of blocks, are both considerably enhanced by the use of procedures that operate on diagrammatic representations. However, Pylyshyn (1973) argues that pictureli”
Handbook of Satisfiability (2021, unknown): “Also notable were the “Logic Theory Machine” of (225) (1957), which used the idea of a search heuristic, and the Geometry machine of (119) (1959), which exploited symmetry to reduce proof size.”