English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The Effectiveness of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary nature of higher-order unification problems, which requires the integration of unification within the calculus and results in a non-effective search for refutations. We present a modification of the constrained resolution calculus (Huet’72) which uses an eager unification algorithm while retaining relative-completeness with regard to bounded unifiers. The first modification is the replacement of the unification rules with that of the bounded unification algorithm in (Ĺıbal’12). This algorithm computes either pre-unifiers, or smaller unification problems which have terms containing Kleene stars. Following a result about an upper bound for these problems (Schmidt-Scauß,Schulz’98), the Kleene stars can effectively be replaced by natural numbers if we are interested in minimal unifiers only and the algorithm then decides the unifiability problem. Since computing minimal unifiers is not enough for the completeness of the calculus, we make a second modification and allow increases of these natural numbers. By applying a semi-eager strategy, we can always eagerly answer the unifiability question of a set of unification constraints while non-minimal unifiers are obtained via back-tracking and the increase of these numbers. P. Fontaine, R.A. Schmidt, S. Schulz (eds.), PAAR-2012 (EPiC Series, vol. 21), pp. 95–95 95

A Resolution Calculus for Second-order Logic with Eager Unification