Mathematical Institute of the Serbian Academy of Sciences and Arts
|Title:||Probabilistic Reasoning about Typed Combinatory Logic||First page:||29||Last page:||31||Related Publication(s):||Book of Abstracts||Conference:||11th International Conference Logic and Applications, LAP 2022, September 26 - 29, 2022||Issue Date:||2022||Rank:||M34||URL:||http://imft.ftn.uns.ac.rs/math/cms/uploads/Main/LAP2022-Book_of_Abstracts.pdf||Abstract:||
In [6, 7] we have introduced a Logic of Combinatory Logic (LCL), a for-
mal system for reasoning about simply typed combinatory terms. The LCL is
obtained by extending the simply typed combinatory logic with classical propo-
sitional connectives, and corresponding axioms and rules. In  we have pre-
sented the syntax, axiomatization and semantics of LCL. The language of the
logic LCL is generated by the following syntax
α, β := M : σ | ¬α | α ∧ β
where M : σ is type assignment statement typable from some basis Γ in
simply typed combinatory logic, M is a combinatory term and σ is a simple type.
The axiomatic system of LCL is obtained by combining the axiomatic system
for classical propositional logic and type assignment system for simply typed
combinatory logic. The semantics for LCL, inspired by Kripke-style semantics
for lambda calculus with types introduced in [8, 5], is based on an extensional
applicative structure containing special elements that correspond to primitive
We have proved that the given axiomatization is sound and complete with
respect to the proposed semantics. Further, we proved that the logic LCL is a
conservative extension of the simply typed combinatory logic.
Our goal is to use the logic LCL to develop a formal system for probabilistic
reasoning about typed combinatory terms. The idea of formal system for rea-
soning about simply typed lambda terms and lambda terms with intersection
types is presented in [2, 3]. These models are based on the well-known models
of lambda calculus, i.e. terms models () and filter models (). However,
these models have shown not to be suitable for propositional reasoning about
typed terms. For this reason, we have developed the logic LCL.
We define PCL, a probabilistic system for simply typed combinatory terms,
as a probabilistic logic over LCL. Formulas of PCL are layered into two sets:
basic formulas and probabilistic formulas. Basic formulas are LCL-formulas.
The set of probabilistic formulas is generated by the following syntax
φ, ψ := P≥aα | ¬φ | φ ∧ ψ
where α is an LCL-formula and s ∈ Q ∩ [0, 1]. The semantics of PCL
are defined as Kripke-style semantics where each world represents one LCL
model. The axiomatic system for PCL is obtained from the axiomatic system
for probability logic and axiomatic system for LCL.
For future work, we plan to prove that the given axiomatization of PCL is
sound and complete with respect to the proposed semantics of PCL. Further,
we plan to investigate probabilistic extensions of other typed calculi.
|Keywords:||Probabilistic reasoning | combinatory logic | simple types | classical propositional logic||Publisher:||University Center Dubrovnik, Croatia||Project:||Advanced artificial intelligence techniques for analysis and design of system components based on trustworthy BlockChain technology - AI4TrustBC|
Show full item record
checked on Mar 20, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.