DC FieldValueLanguage
dc.contributor.authorGhilezan, Silviaen_US
dc.contributor.authorIvetić, Jelenaen_US
dc.contributor.authorKašterović, Simonaen_US
dc.contributor.authorOgnjanović, Zoranen_US
dc.date.accessioned2020-11-25T10:49:35Z-
dc.date.available2020-11-25T10:49:35Z-
dc.date.issued2017-11-
dc.identifier.urihttp://researchrepository.mi.sanu.ac.rs/handle/123456789/4231-
dc.description.abstractWe present a formal model PΛ→ for probabilitic reasoning about simply typed lambda terms, which is a combination of lambda calculus [1] and probabilistic logic [3]. We propose its syntax, Kripke-style semantics and an infinitary axiomatization. We use simple type assignment which is sound and complete ([2]) with respect to the simple semantics (based on the concept of a term model). We define two sets of formulas basic formulas and probabilistic formulas. Basic formulas, denoted by For B, are lambda statements and Boolean combinations of lambda statements. Basic probabilistic formula is any formula of the form P≥sα, such thatα ∈ ForB and s ∈[0,1 ]∩ Q. The set of all probabilistic formulas, denoted by For P, is the smallest set containing all basic probabilistic formulas which is closed under Boolean connectives. The language of PΛ→ consist of both basic formulas and probabilistic formula For PΛ→=For B ∪ For P. Neither mixing of basic formulas and probabilistic formulas, nor nested probability operators is allowed. The following two expressions are not (well defined) formulas of the logic PΛ→: α∧P≥12β, P≥13P≥12α. An axiomatic system for the logic PΛ→ is introduced. It consists of axioms chemes and two groups of inference rules, such that rules from the first group can be applied only on lambda statements. The semantics for PΛ→ is a Kripke-style semantics based on the possible-world approach. The main results are soundness and strong completeness of PΛ→ with respect to the proposed model. We proved strong completeness using the fact that simple type assignment is sound and complete with respect to the simple semantics and property that every consistent set can be extended to a maximal consistent set. The crucial part in the proof of strong completenes is the construction of the canonical model using a maximal consistent set.en_US
dc.publisherMathematical Institute of the SASAen_US
dc.relationDevelopment of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and educationen_US
dc.relationRepresentations of logical structures and formal languages and their application in computingen_US
dc.subjectsimply typed lambda calculus | probabilistic logic | soundness | strong completenessen_US
dc.titleTowards Probabilistic reasoning about simply typed lambda termsen_US
dc.typeConference Paperen_US
dc.relation.conferenceSedma nacionalna konferencija “Verovatnosne logike i njihove primene” ; Beograd, Srbija, 8. novembar 2017en_US
dc.identifier.urlhttp://www.mi.sanu.ac.rs/novi_sajt/research/conferences/vlp2017.pdf-
dc.relation.grantno44006en_US
dc.relation.grantno174026en_US
dc.relation.firstpage11-
dc.relation.lastpage12-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairetypeConference Paper-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.fulltextNo Fulltext-
crisitem.author.orcid0000-0003-2253-8285-
crisitem.author.orcid0000-0003-2508-6480-
crisitem.project.projectURLhttp://www.mi.sanu.ac.rs/novi_sajt/research/projects/044006e.php-
crisitem.project.projectURLhttp://www.mi.sanu.ac.rs/novi_sajt/research/projects/174026e.php-
crisitem.project.fundingProgramNATIONAL HEART, LUNG, AND BLOOD INSTITUTE-
crisitem.project.fundingProgramDirectorate for Social, Behavioral & Economic Sciences-
crisitem.project.openAireinfo:eu-repo/grantAgreement/NIH/NATIONAL HEART, LUNG, AND BLOOD INSTITUTE/5R01HL044006-04-
crisitem.project.openAireinfo:eu-repo/grantAgreement/NSF/Directorate for Social, Behavioral & Economic Sciences/1740267-

#### Page view(s)

30
checked on Feb 3, 2023