Automated Reasoning

@techreport{RISC6684,
author = {Bruno Buchberger},
title = {{Is ChatGPT Smarter Than Master’s Applicants?}},
language = {English},
abstract = {During the selection procedure for a particular informatics fellowship program sponsored by Upper Austrian companies, I ask the applicants a couple of simple technical questions about programming, etc., in a Zoom meeting. I put the same questions to the dialogue system ChatGPT, [ChatGPT]. The result surprised me: Nearly all answers of ChatGPT were totally correct and nicely explained. Also, in the dialogues to clarify some critical points in the answers, the explanations by ChatGPT were amazingly clear and goal-oriented.In comparison: I tried out the same questions in the personal Zoom interviews with approximately 30 applicants from five countries. Only the top three candidates (with a GPA of 1.0, i.e., the highest possible GPA in their bachelor’s study) performed approximately equally well in the interview. All the others performed (far) worse than ChatGPT. And, of course, all answers from ChatGPT came within 1 to 10 seconds, whereas most of the human applicants' answers needed lengthy and arduous dialogues.I am particularly impressed by the ability of ChatGPT to extract meaningful and well-structured programs from problem specifications in natural language. In this experiment, I also added some questions that ask for proofs for simple statements in natural language, which I do not ask in the student's interviews. The performance of ChatGPT was quite impressive as far as formalization and propositional logic are concerned. In examples where predicate logic reasoning is necessary, the ChatGPT answers are not (yet?) perfect. I am pleased to see that ChatGPT tries to present the proofs in a “natural style” This is something that I had as one of my main goals when I initiated the Theorema project in 1995. I think we already achieved this in the early stage of Theorema, and we performed this slightly better and more systematically than ChatGPT does.I also tried to develop a natural language input facility for Theorema in 2017, i.e., a tool to formalize natural language statements in predicate logic. However, I could not continue this research for a couple of reasons. Now I see that ChatGPT achieved this goal. Thus, I think that the following combination of methods could result in a significant leap forward:- the “natural style” proving methods that we developed within Theorema (for the automated generation of programs from specifications, the automated verification of programs in the frame of knowledge, and the automated proof of theorems in theories), in particular, my “Lazy Thinking Method” for algorithm synthesis from specifications- and the natural language formalization techniques of ChatGPT.I propose this as a research project topic and invite colleagues and students to contact me and join me in this effort: Buchberger.bruno@gmail.com.},
number = {23-04},
year = {2023},
month = {January},
keywords = {ChatGPT, automated programming, program synthesis, automated proving, formalization of natural language, master's screening},
length = {30},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC6505,
author = {Temur Kutsia and Cleo Pau},
title = {{A framework for approximate generalization in quantitative theories}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms, retaining their common structure and abstracting differences by variables. We study quantitative anti-unification where the notion of the common structure is relaxed into "proximal'' up to the given degree with respect to the given fuzzy proximity relation. Proximal symbols may have different names and arities. We develop a generic set of rules for computing minimal complete sets of approximate generalizations and study their properties. Depending on the characterizations of proximities between symbols and the desired forms of solutions, these rules give rise to different versions of concrete algorithms.},
number = {22-04},
year = {2022},
month = {May},
keywords = {Generalization, anti-unification, quantiative theories, fuzzy proximity relations},
length = {22},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC6517,
author = {Wolfgang Schreiner},
title = {{The RISCTP Theorem Proving Interface - Tutorial and Reference Manual (Version 1.0.*)}},
language = {english},
abstract = {This report documents the RISCTP theorem proving interface. RISCTP consists of alanguage for specifying proof problems and of an associated software for solving theseproblems. The RISCTP language is a typed variant of first-order logic whose level ofabstraction is between that of higher level formal specification languages (such as thelanguage of the RISCAL model checker) and lower level theorem proving languages (such asthe language SMT-LIB supported by various satisfiability modulo theories solvers such as Z3).Thus the RISCTP language can serve as an intermediate layer that simplifies the connectionof specification and verification systems to theorem provers; in fact, it was developed toequip the RISCAL model checker with theorem proving capabilities. The RISCTP softwareis implemented in Java with an API that enables the implementation of such connections;however, RISCTP also provides a text-based frontend that allows its use as a theorem proveron its own. RISCTP already implements a backend that translates a proving problem intoSMT-LIB and solves it by the "black box" application of Z3; in the future, RISCTP shall alsoprovide built-in proving capabilities with greater transparency.},
number = {22-07},
year = {2022},
month = {June},
keywords = {automated reasoning, theorem proving, model checking, first-order logic, RISCAL, SMT-LIB, Z3},
length = {31},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC6293,
author = {Tudor Jebelean},
title = {{A Heuristic Prover for Elementary Analysis in Theorema}},
language = {english},
abstract = {We present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions, and continuity of the composition of functions.},
number = {21-07},
year = {2021},
month = {April},
keywords = {Theorema, S-decomposition, automated theorem proving},
length = {29},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}