Classical Proofs as Parallel Programs [PDF]
Electronic Proceedings in Theoretical Computer Science, 2018 We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. The
Federico Aschieri +2 more
doaj +5 more sources
Uniform Proofs of Normalisation and Approximation for Intersection Types [PDF]
Electronic Proceedings in Theoretical Computer Science, 2015 We present intersection type systems in the style of sequent calculus, modifying the systems that Valentini introduced to prove normalisation properties without using the reducibility method.
Kentaro Kikuchi
doaj +4 more sources
Natural Deduction for Four-Valued both Regular and Monotonic Logics
, 2017 The development of recursion theory motivated Kleene for creation of three-valued regular logics. Later on taking his inspiration from the computer science, Fitting continued investigations of three-valued regular logics and defined them as monotonic ...
Yaroslav Petrukhin
openalex +3 more sources
On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC [PDF]
Logical Methods in Computer Science, 2017 Dummett's logic LC is intuitionistic logic extended with Dummett's axiom: for every two statements the first implies the second or the second implies the first.
Federico Aschieri
doaj +3 more sources
Strong Normalization for Truth Table Natural Deduction
Fundamenta Informaticae, 2019 We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction. In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic ...
Herman Geuvers +2 more
openalex +3 more sources
Natural Deduction for Three-Valued Regular Logics [PDF]
, 2016 In this paper, I consider a family of three-valued regular logics: the well-known strong and weak S.C. Kleene’s logics and two intermedi- ate logics, where one was discovered by M.
Petrukhin, Yaroslav
core +3 more sources
Application of natural deduction in Renaissance geometry [PDF]
Argument, 2014 My goal here is to provide a detailed analysis of the methods of inference that are employed in De prospectiva pingendi. For this purpose, a method of natural deduction is proposed.
Ryszadr Mirek
doaj +4 more sources
Enhancing cybersecurity through autonomous knowledge graph construction by integrating heterogeneous data sources [PDF]
PeerJ Computer ScienceCybersecurity plays a critical role in today’s modern human society, and leveraging knowledge graphs can enhance cybersecurity and privacy in the cyberspace.
Hatoon Alharbi +3 more
doaj +3 more sources
On an ecumenical natural deduction with stoup - Part I: The propositional case [PDF]
Perspectives on Deduction, 2022 Natural deduction systems, as proposed by Gentzen and further studied by Prawitz, is one of the most well known proof-theoretical frameworks. Part of its success is based on the fact that natural deduction rules present a simple characterization of ...
L. C. Pereira, Elaine Pimentel
semanticscholar +1 more source
Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic [PDF]
Studia Logica: An International Journal for Symbolic Logic, 2021 The tetravalent modal logic (TML\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin ...
M. Figallo
semanticscholar +1 more source