HOL-λσ: an intentional first-order expression of higher-order logic
From MaRDI portal
Publication:2713352
DOI10.1017/S0960129500003236zbMath0972.03012OpenAlexW2023145007MaRDI QIDQ2713352
Thérèse Hardin, Gilles Dowek, Claude Kirchner
Publication date: 13 November 2001
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129500003236
explicit substitutionsproof-searchExtended Narrowing and Resolutionfirst-order presentation of higher-order logicsimulation of higher-order resolution
Related Items
Rewriting logic: Roadmap and bibliography, Nominal logic, a first order theory of names and binding, Twenty years of rewriting logic, A semantic framework for proof evidence, Theorem proving modulo, Narrowing Based Inductive Proof Search, A simple proof that super-consistency implies cut elimination, Resolution is cut-free, Regaining cut admissibility in deduction modulo using abstract completion, Experimenting with Deduction Modulo, Axiom Directed Focusing, Inductive proof search modulo, Automating Theories in Intuitionistic Logic