Application of Theorem Proving to Problem Solving

By C. Green. 1969

Subfields: 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 Automated Theorem Proving & Formal Methods

Citations in the corpus

Optimal Ordered Problem Solver (2002, neutral): “Unlike logic-based program synthesizers (Green, 1969, Waldinger and Lee, 1969, Deville and Lau, 1994), program evolvers use biology-inspired concepts of Evolutionary Computation (Rechenberg, 1971, Schwefel, 1974) or Genetic Algorithms (Holland, 1975) to evolve better and better computer programs.”
STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving (1971, methodology): “INTRODUCTION This paper describes a new problem-solving program called STRIPS (STanford Research Institute Problem Solver).”
Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation (2023, methodology): “program synthesis techniques have been developed, including deductive synthesis [18, 31, 53], programming by examples [19, 48] and neural-guided synthesis [25].”
Acquiring Recursive and Iterative Concepts with Explanation-Based Learning (1990, methodology): “The situation calculus (McCarthy, 1963) is used in this section’s example to reason about actions, in the style of Green (1969).”
Structural Language Models of Code (2019, background): “Typically, the task is to generate a program given some form of input or context, such as complete formal specifications (Green, 1981; Si et al., 2019) or input-output examples (Gulwani, 2011; Devlin et al.”
Understanding natural language (1972, methodology): “UNDERSTANDING NATURAL LANGUAGE 39 The “uniform procedure” approach was adopted by a number of systems (see discussion in Green, 1968, 1969) as an alternative to the kind of specialized limited logic discussed in the previous section.”
Bayesian Sketch Learning for Program Synthesis (2017, background): “The automatic synthesis of programs [11, 18, 29, 47] is a long-standing goal in computer science.”
An Empirical Study of the Non-Determinism of ChatGPT in Code Generation (2023, unknown): “When setting temperature=0, the code candidates generated from the Concise prompt are more deterministic than our Base prompt, while those code candidates generated from the CoT prompt suffer from higher randomness than our Base prompt.”
Perception as Abduction: Turning Sensor Data Into Meaningful Representation (2005, background): “However, one of the finest early attempts to use logic and theorem proving in the way described, namely Green’s resolution-based planner ( Green, 1969 ), fell foul of computational complexity problems.”
Toward automatic program synthesis (1971, methodology): “ture (e.g. Green [ 6 , 7], Waldinger and Lee [29], Waldinger [28], and Luckham and Nilsson [12]).”
An Empirical Study of Code Smells in Transformer-based Code Generation Techniques (2022, background): “[47] surveyed the foundation of program synthesis, such as the deductive synthesis approach [48], [49], in which task specification is converted into constraints and extracts the program after proving the constraint satisfaction.”
Using temporal logics to express search control knowledge for planning (2000, methodology): “We have implemented our ideas in the TLPLAN system, and have been able to demonstrate its remarkable effectiveness in a wide range of planning domains.”
Structural Language Models for Any-Code Generation (2019, background): “Typically, the task is to generate a program given some form of input or context, such as complete formal speciﬁcations (Green, 1981) or input-output examples (Gulwani, 2011; Devlin et al., 2017; Parisotto et al., 2017).”