HOL-λσ: an intentional first-order expression of higher-order logic
From MaRDI portal
Publication:2713352
DOI10.1017/S0960129500003236zbMath0972.03012MaRDI QIDQ2713352
Gilles Dowek, Claude Kirchner, Thérèse Hardin
Publication date: 13 November 2001
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
explicit substitutions; proof-search; Extended Narrowing and Resolution; first-order presentation of higher-order logic; simulation of higher-order resolution
03B35: Mechanization of proofs and logical operations
Related Items
Theorem proving modulo, Rewriting logic: Roadmap and bibliography, Nominal logic, a first order theory of names and binding