scholarly journals Normalisation for higher-order calculi with explicit substitutions

2005 ◽  
Vol 333 (1-2) ◽  
pp. 91-125
Author(s):  
Eduardo Bonelli
Keyword(s):  
Higher Order ◽  
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

Dual systems for all: Higher-order, role-based relational reasoning as a uniquely derived feature of human cognition

2019 ◽  
Vol 42 ◽  
Author(s):  
Daniel J. Povinelli ◽  
Gabrielle C. Glorioso ◽  
Shannon L. Kuznar ◽  
Mateja Pavlic
Keyword(s):  
Temporal Reasoning ◽  
Higher Order ◽  
Important Case ◽  
Human Cognition ◽  
Relational Reasoning ◽  
Dual Systems ◽  
First Order ◽  
Reasoning System ◽  
Role Based

Abstract Hoerl and McCormack demonstrate that although animals possess a sophisticated temporal updating system, there is no evidence that they also possess a temporal reasoning system. This important case study is directly related to the broader claim that although animals are manifestly capable of first-order (perceptually-based) relational reasoning, they lack the capacity for higher-order, role-based relational reasoning. We argue this distinction applies to all domains of cognition.

Sign in / Sign up

Export Citation Format

Share Document