Annals of Pure and Applied Logic 39 (2):131-174 (1988)

This paper presents an algorithm that, given a finite set E of pairs of second-order monadic terms, returns a finite set U of ‘substitution schemata’ such that a substitution unifies E iff it is an instance of some member of U . Moreover, E is unifiable precisely if U is not empty. The algorithm terminates on all inputs, unlike the unification algorithms for second-order monadic terms developed by G. Huet and G. Winterstein. The substitution schemata in U use expressions which represent sets of terms that differ only in how many times designated strings of function constants follow themselves. The substitution schemata may contain unresolved ‘identity restrictions’; consequently, the members of U generally do not characterize all the unifiers of E in a completely explicit way. The algorithm is particularly useful for investigating the complexity of formal proofs
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(88)90015-2
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 59,775
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

A Machine-Oriented Logic Based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.

Add more references

Citations of this work BETA

The Undecidability of K-Provability.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 53 (1):75-102.
Bounded Arithmetic, Proof Complexity and Two Papers of Parikh.Samuel R. Buss - 1999 - Annals of Pure and Applied Logic 96 (1-3):43-55.
Generalizing Proofs in Monadic Languages.Matthias Baaz & Piotr Wojtylak - 2008 - Annals of Pure and Applied Logic 154 (2):71-138.

Add more citations

Similar books and articles

Involutions Defined by Monadic Terms.Renato A. Lewin - 1988 - Studia Logica 47 (4):387 - 389.
The Undecidability of the Second Order Predicate Unification Problem.Gilles Amiot - 1990 - Archive for Mathematical Logic 30 (3):193-199.
Random Graphs in the Monadic Theory of Order.Shmuel Lifsches & Saharon Shelah - 1999 - Archive for Mathematical Logic 38 (4-5):273-312.
Higher Order Unification and the Interpretation of Focus.Stephen G. Pulman - 1997 - Linguistics and Philosophy 20 (1):73-115.


Added to PP index

Total views
3 ( #1,300,460 of 2,432,669 )

Recent downloads (6 months)
1 ( #464,745 of 2,432,669 )

How can I increase my downloads?


My notes