Theorem Proving in Higher-Order Logics
- Theorem Proving in Higher-Order Logics
Theorem Proving in Higher-Order Logics (TPHOLs) is an annual international academic conference on the topic of automated reasoning in higher-order logics. The first TPHOLs was held in Cambridge, UK in 1987, but in the early years was an informal gathering of researchers interested in the HOL system and had no formal proceedings. Since 1990 TPHOLs has published formal peer-reviewed proceedings, published by Springer's LNCS series.
TPHOLs brings together the communities using many systems based on higher-order logic such as Coq, Isabelle, NuPRL, PVS, and Twelf. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference.
Together with CADE and TABLEAUX, TPHOLs is usually one of the three main conferences of the International Joint Conference on Automated Reasoning (IJCAR) whenever it convenes,
In 2006, TPHOLs was part of the Federated Logic Conference held in Seattle, USA.
External links
* [http://www.cl.cam.ac.uk/Research/HVG/HOL/ Home-page of the HOL group] at the University of Cambridge, the traditional home of TPHOLs.
Wikimedia Foundation.
2010.
Look at other dictionaries:
Higher-order abstract syntax — In computer science, higher order abstract syntax (abbreviated HOAS) is a technique for the representation of abstract syntax trees for languages with variable binders.Relation to first order abstract syntaxAn abstract syntax tree is abstract… … Wikipedia
Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… … Wikipedia
Isabelle (theorem prover) — Infobox Software name = Isabelle caption = collapsible = author = developer = released = latest release version = latest release date = latest maintenance version = latest maintenance date = latest preview version = latest preview date =… … Wikipedia
First-order logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… … Wikipedia
Gödel's completeness theorem — is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first order logic. It was first proved by Kurt Gödel in 1929. A first order formula is called logically valid if… … Wikipedia
Herbrand's theorem — is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). [J. Herbrand: Recherches sur la theorie de la demonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et… … Wikipedia
Michael J. C. Gordon — Born February 28, 1948 (1948 02 28) (age 63) … Wikipedia
HOL theorem prover family — HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language … Wikipedia
Federated Logic Conference — The Federated Logic Conference (FLoC) is an international conglomeration of several mathematical logic and computer science related academic conferences that deal with the intersection of the two fields. FLoC traditionally includes:* Logic in… … Wikipedia
LNCS1125 — J. von Wright/J. Grundy/J. Harrison (Eds.): Theorem Proving in Higher Order Logics, Springer Verlag Proceedings 1996 … Acronyms
