External links
| International | |
|---|---|
| National | |
Interactive Theorem Proving (ITP) is an annual international academic conference on the topic of automated theorem proving, proof assistants and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.
ITP brings together the communities using many systems based on higher-order logic such as ACL2, Coq, Mizar, HOL, Isabelle, Lean, NuPRL, PVS, and Twelf. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference.
Together with CADE and TABLEAUX, ITP is usually one of the three main conferences of the International Joint Conference on Automated Reasoning (IJCAR) whenever it convenes,
The inaugural meeting of ITP was held on 11–14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference. It is the extension of the Theorem Proving in Higher Order Logics (TPHOLs) conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009.
The first three were informal users' meetings for the HOL system and were the only ones without published papers. Since 1990 TPHOLs has published formal peer-reviewed proceedings, published by Springer's Lecture Notes in Computer Science series. It has also entertained an increasingly wide field of interest.
| International | |
|---|---|
| National | |
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.
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
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.
HOL denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defines an abstract data type of proven theorems such that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. As such, a large system can be built on top of a small trusted kernel.
Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.
Michael John Caldwell Gordon was a British computer scientist.
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.
The International Joint Conference on Automated Reasoning (IJCAR) is a series of conferences on the topics of automated reasoning, automated deduction, and related fields. It is organized semi-regularly as a merger of other meetings. IJCAR replaces those independent conferences in the years it takes place. The conference is organized by CADE Inc., and CADE has always been one of the conferences partaking in IJCAR.
The drinker paradox is a theorem of classical predicate logic that can be stated as "There is someone in the pub such that, if he or she is drinking, then everyone in the pub is drinking." It was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his 1978 book What Is the Name of this Book?
The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) is an annual international academic conference that deals with all aspects of automated reasoning with analytic tableaux. Periodically, it joins with CADE and TPHOLs into the International Joint Conference on Automated Reasoning (IJCAR).
In programming language theory, the POPLmark challenge is a set of benchmarks designed to evaluate the state of automated reasoning in the metatheory of programming languages, and to stimulate discussion and collaboration among a diverse cross section of the formal methods community. Very loosely speaking, the challenge is about measurement of how well programs may be proven to match a specification of how they are intended to behave. The challenge was initially proposed by the members of the PL club at the University of Pennsylvania, in association with collaborators around the world. The Workshop on Mechanized Metatheory is the main meeting of researchers participating in the challenge.
Geoff Sutcliffe is a US-based computer scientist working in the field of automated reasoning. He was born in the former British colony of Northern Rhodesia , grew up in South Africa, and earned his PhD in Australia. Sutcliffe currently works at the University of Miami, and is of both British and Australian nationality.
The Vienna Summer of Logic was a scientific event in the summer of 2014, combining 12 major conferences and several workshops from the fields of mathematical logic, logic in computer science, and logic in artificial intelligence. The meetings took place from July 9 to 24, 2014, and attracted more than 2000 scientists and researchers.
Tobias Nipkow is a German computer scientist.
Grigore Roșu is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in the Information Trust Institute. He is known for his contributions in runtime verification, the K framework, matching logic, and automated coinduction.
