Theorem Proving in Higher-Order Logics
Encyclopedia
Theorem Proving in Higher-Order Logics (TPHOLs) is an annual international academic conference
on the topic of automated reasoning
in higher-order logic
s. 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
(FLoC) held in Seattle, USA.
TPHOLs is superseded by the international conference on Interactive Theorem Proving (ITP), which combines the old TPHOLs with the ACL2 Workshop series.
The first ITP meeting was in 2010, held as part of FLoC in Edinburgh
, Scotland
.
Academic conference
An academic conference or symposium is a conference for researchers to present and discuss their work. Together with academic or scientific journals, conferences provide an important channel for exchange of information between researchers.-Overview:Conferences are usually composed of various...
on the topic of automated reasoning
Automated reasoning
Automated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically...
in higher-order logic
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
s. The first TPHOLs was held in Cambridge
Cambridge
The city of Cambridge is a university town and the administrative centre of the county of Cambridgeshire, England. It lies in East Anglia about north of London. Cambridge is at the heart of the high-technology centre known as Silicon Fen – a play on Silicon Valley and the fens surrounding the...
, UK
United Kingdom
The United Kingdom of Great Britain and Northern IrelandIn the United Kingdom and Dependencies, other languages have been officially recognised as legitimate autochthonous languages under the European Charter for Regional or Minority Languages...
in 1987, but in the early years was an informal gathering of researchers interested in the HOL
HOL theorem prover
HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....
system and had no formal proceedings. Since 1990 TPHOLs has published formal peer-reviewed proceedings, published by Springer
Springer Science+Business Media
- Selected publications :* Encyclopaedia of Mathematics* Ergebnisse der Mathematik und ihrer Grenzgebiete * Graduate Texts in Mathematics * Grothendieck's Séminaire de géométrie algébrique...
's LNCS
Lecture Notes in Computer Science
Lecture Notes in Computer Science is a series of computer science books that has been published by Springer Science+Business Media since 1973....
series.
TPHOLs brings together the communities using many systems based on higher-order logic such as Coq
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
, Isabelle
Isabelle theorem prover
The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic theorem prover. It is an LCF-style theorem prover , so it is based on a small logical core guaranteeing logical correctness...
, NuPRL
NuPRL
NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL....
, PVS
Prototype Verification System
The Prototype Verification System is a specification language integrated with support tools and a theorem prover.It was developed at the Computer Science Laboratory of SRI International in California. PVS is based on a kernel consisting of an extension of Church's theory of types with dependent...
, and Twelf
Twelf
Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.-Introduction:...
. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference.
Together with CADE
Conference on Automated Deduction
The Conference on Automated Deduction is the premier academic conference on automated deduction and related fields. The first CADE was organized in 1974 at the Argonne National Laboratory near Chicago. Most CADE meetings have been held in Europe and the USA. However, conferences have been held all...
and TABLEAUX, TPHOLs is usually one of the three main conferences of the International Joint Conference on Automated Reasoning
International Joint Conference on Automated Reasoning
International Joint Conference on Automated Reasoning 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...
(IJCAR) whenever it convenes,
In 2006, TPHOLs was part of the Federated Logic Conference
Federated Logic Conference
The Federated Logic Conference is an international conglomeration of several mathematical logic and computer science related academic conferences that deal with the intersection of the two fields...
(FLoC) held in Seattle, USA.
TPHOLs is superseded by the international conference on Interactive Theorem Proving (ITP), which combines the old TPHOLs with the ACL2 Workshop series.
The first ITP meeting was in 2010, held as part of FLoC in Edinburgh
Edinburgh
Edinburgh is the capital city of Scotland, the second largest city in Scotland, and the eighth most populous in the United Kingdom. The City of Edinburgh Council governs one of Scotland's 32 local government council areas. The council area includes urban Edinburgh and a rural area...
, Scotland
Scotland
Scotland is a country that is part of the United Kingdom. Occupying the northern third of the island of Great Britain, it shares a border with England to the south and is bounded by the North Sea to the east, the Atlantic Ocean to the north and west, and the North Channel and Irish Sea to the...
.
External links
- Home-page of the HOL group at the University of CambridgeUniversity of CambridgeThe University of Cambridge is a public research university located in Cambridge, United Kingdom. It is the second-oldest university in both the United Kingdom and the English-speaking world , and the seventh-oldest globally...
, the traditional home of TPHOLs.