IBM Neuro-Symbolic AI Summer School Day 1: ULKB Logic Language (Guilherme Lima)
NLP
NLU
knowledge graphs
conference
Typed lambda-calculus with logical connectives and quantifiers, HOL kernel, easy Python interface.

IBM NeuroSymbolicAI Summer School 2022 Day 1: ULKB (Universal Logic Knowledge Base) Logic Language given by Guilherme Lima:
Typed lambda-calculus with equality plus logical connectives (negation, and, or, conditional, biconditional) and quantifiers (exists, for all)
Has expressions (terms, formulas, types), annotations, and theories (axioms, theorems, definitions)
HOL (Higher Order Logic) kernel supports substitution, reduction and inference rules.
Easy to use Python interface.
Summer School site: https://ibm.github.io/neuro-symbolic-ai/events/ns-summerschool2022/
Originally posted on LinkedIn.