Higher-order equational unification via explicit substitutions

1997 ◽  
pp. 61-75 ◽  
Author(s):  
Claude Kirchner ◽  
Christophe Ringeissen
Keyword(s):  
Higher Order ◽  
Equational Unification ◽  
Explicit Substitutions

scholarly journals Higher Order Unification via Explicit Substitutions

2000 ◽  
Vol 157 (1-2) ◽  
pp. 183-235 ◽  
Author(s):  
Gilles Dowek ◽  
Thérèse Hardin ◽  
Claude Kirchner
Keyword(s):  
Higher Order ◽  
Explicit Substitutions

scholarly journals HOL-λσ: an intentional first-order expression of higher-order logic

2001 ◽  
Vol 11 (1) ◽  
pp. 21-45 ◽  
Author(s):  
GILLES DOWEK ◽  
THERESE HARDIN ◽  
CLAUDE KIRCHNER
Keyword(s):  
Order Theory ◽  
Higher Order ◽  
Search Method ◽  
Order Logic ◽  
Automated Deduction ◽  
Higher Order Logic ◽  
First Order ◽  
Proof Search ◽  
First Order Theory ◽  
Explicit Substitutions

We give a first-order presentation of higher-order logic based on explicit substitutions. This presentation is intentionally equivalent to the usual presentation of higher-order logic based on λ-calculus, that is, a proposition can be proved without the extensionality axioms in one theory if and only if it can be in the other. We show that the Extended Narrowing and Resolution first-order proof-search method can be applied to this theory. In this way we get a step-by-step simulation of higher-order resolution. Hence, expressing higher-order logic as a first-order theory and applying a first-order proof search method is a relevant alternative to a direct implementation. In particular, the well-studied improvements of proof search for first-order logic could be reused at no cost for higher-order automated deduction. Moreover, as we stay in a first-order setting, extensions, such as equational higher-order resolution, may be easier to handle.

scholarly journals Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions

2008 ◽  
Vol 6 (1) ◽  
pp. 72-108 ◽  
Author(s):  
Flávio L.C. de Moura ◽  
Mauricio Ayala-Rincón ◽  
Fairouz Kamareddine
Keyword(s):  
Higher Order ◽  
Structural Relation ◽  
Explicit Substitutions ◽  
The One

Explicit substitutions and higher-order syntax

2006 ◽  
Vol 19 (2-3) ◽  
pp. 263-282 ◽  
Author(s):  
Neil Ghani ◽  
Tarmo Uustalu ◽  
Makoto Hamana
Keyword(s):  
Higher Order ◽  
Explicit Substitutions
Sign in / Sign up

Export Citation Format

Share Document