Proof theory – Workshop on Trends, Extensions, Applications and Semantics of Logic Programming https://www.coalg.org/tease-lp TEASE-LP, 28 and 29 May 2020, Virtual Event Wed, 27 May 2020 20:57:17 +0000 en-GB hourly 1 https://wordpress.org/?v=6.1.1 Dale Miller: Structural Proof-Theory and Logic Programming https://www.coalg.org/tease-lp/2020/dale-miller-structural-proof-theory-and-logic-programming/ https://www.coalg.org/tease-lp/2020/dale-miller-structural-proof-theory-and-logic-programming/#respond Thu, 14 May 2020 20:16:46 +0000 https://www.coalg.org/tease-lp/?p=181 We discuss the influences of structural proof theory on logic programming and vice versa.

Forum    Abstract

Attachments

]]> https://www.coalg.org/tease-lp/2020/dale-miller-structural-proof-theory-and-logic-programming/feed/ 0 Vivek Nigam: A Proof Theory for Distributed Evidential Transactions https://www.coalg.org/tease-lp/2020/a-proof-theory-for-distributed-evidential-transactions/ https://www.coalg.org/tease-lp/2020/a-proof-theory-for-distributed-evidential-transactions/#respond Thu, 14 May 2020 12:36:33 +0000 https://www.coalg.org/tease-lp/?p=108 Evidential transactions (ETs) provide auditable and composable evidence that serves as a witness or a proof that a transaction has been correctly executed by the named parties. For example, for issuing a Visa, an applicant demonstrates, among other evidence, that he has sufficient financial means to visit a foreign country. The form of evidence in ETs has traditionally been unstructured and informal, in the form of paper-based evidence. This paper proposes a formal treatment of evidence based on proof theory. In particular, we investigate the proof theory of Cyberlogic, an assertion logic for ETs, that enables the combination of evidence represented as logical derivations and as digital certificates, i.e., electronic evidence signed by a principal’s secret key. We propose a proof system for Cyberlogic, refining it with further constructions that support a wider range of ETs. We prove that the proof system admits cut-elimination.

Moreover, we propose a sound and complete focused proof system for the refinement of Cyberlogic thus enabling efficient proof-search. Furthermore, we identify a fragment of Cyberlogic, called Cyberlogic Programs, that can be used to efficiently program ETs using a variety of FOL engines. Finally, we propose Proof Certificate format for Cyberlogic Programs inspired by Foundational Proof Certificates as a means to communicate evidence and check its validity.

This is joint work with Giselle Reis, Harald Ruess, Dian Balta, Tewodros Beyene, and Natarajan Shankar.

Forum Full Abstract

Attachments

]]> https://www.coalg.org/tease-lp/2020/a-proof-theory-for-distributed-evidential-transactions/feed/ 0