52 citations · 145 across the 52 of their papers we have counts for
5 papers · 1 filter
Proof Relevant Corecursive Resolution
Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers +1
Resolution lies at the foundation of both logic programming and type class context reduction in functional languages. Terminating derivations by resolution have well-defined induct…
Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
Ekaterina Komendantskaya, Patricia Johann, Martin Schmidt
Logic programming (LP) is a programming language based on first-order Horn clause logic that uses SLD-resolution as a semi-decision procedure. Finite SLD-computations are inductive…
A Type-Theoretic Approach to Resolution
Peng Fu, Ekaterina Komendantskaya
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction o…
Structural Resolution for Logic Programming
P. Johann, E. Komendantskaya, V. Komendantskiy
We introduce a Three Tier Tree Calculus (3TC) that defines in a systematic way three tiers of tree structures underlying proof search in logic programming. We use 3TC to define a n…
A Type-Theoretic Approach to Structural Resolution
Peng Fu, Ekaterina Komendantskaya
Structural resolution (or S-resolution) is a newly proposed alternative to SLD-resolution that allows a systematic separation of derivations into term-matching and unification step…