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

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

zbMATH Keywords

explicit substitutionsproof-searchExtended Narrowing and Resolutionfirst-order presentation of higher-order logicsimulation of higher-order resolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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