Research group

Programming Languages and Tools Lab

Semantics of First-order Horn Clause Logic

September 10

Semantics of First-order Horn Clause Logic

🕑  13 сентября 2021г. (понедельник), 17:30 МСК

🗣  Yue LI

📃  First-order Horn clauses (Horn clause for short) are logic formulae of the shape "A0 <- A1, A2, ..., An"  where the A's are atomic formulae of the shape "p(t1, t2, ..., tn)",  where the p is a predicate symbol and the t's are first-order terms. A finite set of Horn clauses is called a logic program, which can intuitively encode and solve logic puzzles such as the "N-queens problem". Given a logic program, we are interested in what logical truth can be derived from it, and how to derive the truth; these interests are formally known as (respectively) the "denotational semantics"  and "operational semantics" of logic programs. Actually, not all logical deductions terminate (chicken or egg, which comes the first?), and this gives rise to a notion more general than "that which can be derived", viz. "that which cannot be refuted" — we call the two kinds of truth "inductive truth" and "coinductive truth" respectively. A piece of inductive truth is always a piece of coinductive truth, but not vice versa. Correspondingly, the denotational and operational semantics of logic programs can be classified into "inductive" and "coinductive". The denotational semantics enjoy a stronger mathematical flavour, and thanks to that, researchers since as early as 70's are aware of the denotational semantics in both inductive and coinductive senses (as least and greatest fixed points of monotone operators over complete lattices). However, the operational semantics is more algorithm-oriented, and it is only since 2000's that coinductive operational semantics emerge. I shall explain with some more details about these semantics and their interrelationship, and introduce the latest development in coinductive operational semantics, in which I participated.  

🇷🇺  Язык встречи: английский

🔗  Ссылка на встречу: