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 impetus for the development of computer science.
In mathematics, a Boolean ringR is a ring for which x2 = x for all x in R, that is, a ring that consists of only idempotent elements. An example is the ring of integers modulo 2.
In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution.
E is a high-performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
Hendrik Pieter (Henk) Barendregt is a Dutch logician, known for his work in lambda calculus and type theory.
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.
The Handbook of Automated Reasoning is a collection of survey articles on the field of automated reasoning. Published in June 2001 by MIT Press, it is edited by John Alan Robinson and Andrei Voronkov. Volume 1 describes methods for classical logic, first-order logic with equality and other theories, and induction. Volume 2 covers higher-order, non-classical and other kinds of logic.
David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill.
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.
Bruno Courcelle is a French mathematician and computer scientist, best known for Courcelle's theorem in graph theory.
In mathematics and theoretical computer science, a set constraint is an equation or an inequation between sets of terms. Similar to systems of (in)equations between numbers, methods are studied for solving systems of set constraints. Different approaches admit different operators on sets and different (in)equation relations between set 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.
Tobias Nipkow is a German computer scientist.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
