HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic
Explore this paper's citation graph
Summary
A first-order presentation of higher-order logic based on explicit substitutions, i.e. a proposition can be proved without the extensionality axioms in one theory if and only if it can in the other, is proposed.
- Type
- preprint
- Published
- 1999-07-02
- Cited by
- 7
- References
- 16
- OpenAlex
- https://openalex.org/W49642860
- Semantic Scholar
- https://api.semanticscholar.org/CorpusID:262267345
Keywords
HOL, Higher-order logic, Resolution (logic), Axiom, Order (exchange)
References
- Constrained resolution: a complete method for higher-order logic.
- Rewriting modulo a rewrite system
- Proofs in Higher-Order Logic
- Adventures in sequent calculus modulo equations
- General models, descriptions, and choice in type theory
- A formulation of the simple theory of types
- The Undecidability of Unification in Third Order Logic
- Completion of a set of rules modulo a set of equations
- Complete Sets of Reductions for Some Equational Theories
- Combinatory Reduction Systems: Introduction and Survey
- A compact representation of proofs
- Normalised rewriting and normalised completion
- Higher Order Unification via Explicit Substitutions
- Explicit substitutions
- Resolution in type theory
- An introduction to mathematical logic and type theory - to truth through proof
- Completion of a Set of Rules Modulo a Set of Equations
Cited by
- CINNI - A Generic Calculus of Explicit Substitutions and its Application to lambda-, varsigma- and pi- Calculi
- A Semantic Proof that Reducibility Candidates entail Cut Elimination
- A completeness theorem for strong normalization in minimal deduction modulo
- Complete reducibility candidates
- A semantic method to prove strong normalization from weak normalization
- Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory
- From Higher-Order to First-Order Rewriting