Related Research Articles
Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major motivating factor for the development of computer science.
In logic and computer science, specifically automated reasoning, unification is an algorithmic process of solving equations between symbolic expressions, each of the form Left-hand side = Right-hand side. For example, using x,y,z as variables, and taking f to be an uninterpreted function, the singleton equation set { f(1,y) = f(x,2) } is a syntactic first-order unification problem that has the substitution { x ↦ 1, y ↦ 2 } as its only solution.
The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.
Hendrik Pieter (Henk) Barendregt is a Dutch logician, known for his work in lambda calculus and type theory.
Franz Baader is a German computer scientist at Dresden University of Technology.
In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent.
Rewriting Techniques and Applications (RTA) is an annual international academic conference on the topic of rewriting. It covers all aspects of rewriting, including termination, equational reasoning, theorem proving, higher-order rewriting, unification and the lambda calculus. The conference consists of peer-reviewed papers with the proceedings published by Springer in the LNCS series until 2009, and since then in the LIPIcs series published by the Leibniz-Zentrum für Informatik. Several rewriting-related workshops are also affiliated with RTA.
In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.
John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.
Gérard Pierre Huet is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory and to the theory of computation.
Jan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the algebra of communicating processes, co-author of TeReSe and his fixed point combinator
Anti-unification is the process of constructing a generalization common to two given symbolic expressions. As in unification, several frameworks are distinguished depending on which expressions are allowed, and which expressions are considered equal. If variables representing functions are allowed in an expression, the process is called "higher-order anti-unification", otherwise "first-order anti-unification". If the generalization is required to have an instance literally equal to each input expression, the process is called "syntactical anti-unification", otherwise "E-anti-unification", or "anti-unification modulo theory".
Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions.
Jean-Pierre Jouannaud is a French computer scientist, known for his work in the area of term rewriting.
Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems.
Wayne Snyder is an associate professor at Boston University known for his work in E-unification theory.
Christoph Walther is a German computer scientist, known for his contributions to automated theorem proving. He is Professor emeritus at Darmstadt University of Technology.
In computer science, interference freedom is a technique for proving partial correctness of concurrent programs with shared variables. Hoare logic had been introduced earlier to prove correctness of sequential programs. In her PhD thesis under advisor David Gries, Susan Owicki extended this work to apply to concurrent programs.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
Dale Miller is an American computer scientist and author. He is a Director of Research at Inria Saclay and one of the designers of the λProlog programming language and the Abella interactive theorem prover.
References
- ↑ Blanchette, Jasmin (12 February 2021). "Message from the New Editor-in-Chief". Journal of Automated Reasoning. 65 (2): 155. doi: 10.1007/s10817-021-09587-y . hdl: 1871.1/1216cab9-08c1-4d41-8069-aa1735f5786d .
- ↑ Brief vita
- ↑ "Herbrand Award for Distinguished Contributions to Automated Reasoning". CADE Inc. Retrieved 14 July 2021.
- ↑ "Tobias Nipkow". Member. Academia Europaea. Retrieved 2024-10-03.
