scholarly journals A deep inference system with a self-dual binder which is complete for linear lambda calculus

2014 ◽  
Vol 26 (2) ◽  
pp. 677-698 ◽  
Author(s):  
Luca Roversi
Keyword(s):  
Lambda Calculus ◽  
Inference System ◽  
Deep Inference

scholarly journals Strictness and Totality Analysis

1994 ◽  
Vol 23 (474) ◽  
Author(s):  
Kirsten Lackner Solberg ◽  
Hanne Riis Nielson
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Lambda Calculus ◽  
Inference System

We define a novel inference system for strictness and totality analysis for the simply-typed lazy lambda-calculus with constants and fixpoints. Strictness information identifies those terms that definitely denote bottom (i.e. do not evaluate to WHNF) whereas totality information identifies those terms that definitely do not denote bottom (i.e. do evaluate to WHNF). The analysis is presented as an annotated type system allowing conjunctions only at ``top level´´. We give examples of its use and prove the correctness with respect to a natural-style operational semantics.

scholarly journals Deep inference and expansion trees for second-order multiplicative linear logic

2018 ◽  
Vol 29 (8) ◽  
pp. 1030-1060
Author(s):  
LUTZ STRAßBURGER
Keyword(s):  
Original Work ◽  
Linear Logic ◽  
Second Order ◽  
Inference System ◽  
Herbrand’S Theorem ◽  
Deep Inference ◽  
Herbrand's Theorem

In this paper, we introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.

scholarly journals A Deep Inference System for the Modal Logic S5

Studia Logica ◽  
2007 ◽  
Vol 85 (2) ◽  
pp. 199-214 ◽  
Author(s):  
Phiniki Stouppa
Keyword(s):  
Modal Logic ◽  
Inference System ◽  
Deep Inference

scholarly journals Spinal Atomic Lambda-Calculus

2020 ◽  
pp. 582-601
Author(s):  
David Sherratt ◽  
Willem Heijltjes ◽  
Tom Gundersen ◽  
Michel Parigot
Keyword(s):  
Lambda Calculus ◽  
Proof System ◽  
Natural Properties ◽  
Deep Inference

AbstractWe present the spinal atomic $$\lambda $$ λ -calculus, a typed $$\lambda $$ λ -calculus with explicit sharing and atomic duplication that achieves spinal full laziness: duplicating only the direct paths between a binder and bound variables is enough for beta reduction to proceed. We show this calculus is the result of a Curry–Howard style interpretation of a deep-inference proof system, and prove that it has natural properties with respect to the $$\lambda $$ λ -calculus: confluence and preservation of strong normalisation.

Lambda Calculus with Types

2009 ◽  
Author(s):  
Henk Barendregt ◽  
Wil Dekkers ◽  
Richard Statman
Keyword(s):  
Lambda Calculus

Aplikasi Peramalan Kebutuhan Beban Listrik Menggunakan Metode Adaptive Neuro Fuzzy Inference System (ANFIS)

2017 ◽  
Vol 3 (1) ◽  
pp. 36-48
Author(s):  
Erwan Ahmad Ardiansyah ◽  
Rina Mardiati ◽  
Afaf Fadhil
Keyword(s):  
Fuzzy Inference System ◽  
Fuzzy Inference ◽  
Inference System ◽  
Neuro Fuzzy

Prakiraan atau peramalan beban listrik dibutuhkan dalam menentukan jumlah listrik yang dihasilkan. Ini menentukan  agar tidak terjadi beban berlebih yang menyebabkan pemborosan atau kekurangan beban listrik yang mengakibatkan krisis listrik di konsumen. Oleh karena itu di butuhkan prakiraan atau peramalan yang tepat untuk menghasilkan energi listrik. Teknologi softcomputing dapat digunakan  sebagai metode alternatif untuk prediksi beban litrik jangka pendek salah satunya dengan metode  Adaptive Neuro Fuzzy Inference System pada penelitian tugas akhir ini. Data yang di dapat untuk mendukung penelitian ini adalah data dari APD PLN JAWA BARAT yang berisikan laporan data beban puncak bulanan penyulang area gardu induk majalaya dari januari 2011 sampai desember 2014 sebagai data acuan dan data aktual januari-desember 2015. Data kemudian dilatih menggunakan metode ANFIS pada software MATLAB versi b2010. Dari data hasil pelatihan data ANFIS kemudian dilakukan perbandingan dengan data aktual dan data metode regresi meliputi perbandingan anfis-aktual, regresi-aktual dan perbandingan anfis-regresi-aktual. Dari perbandingan disimpulkan bahwa data metode anfis lebih mendekati data aktual dengan rata-rata 1,4%, menunjukan prediksi ANFIS dapat menjadi referensi untuk peramalan beban listrik dimasa depan.

Sign in / Sign up

Export Citation Format

Share Document