Higher-order superposition for dependent types

DOI10.1007/3-540-61464-8_47zbMATH Open1504.68093OpenAlexW1565847800MaRDI QIDQ5055856FDOQ5055856

Authors: Roberto Virga 

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61464-8_47

Recommendations

• Rewriting Techniques and Applications
• Higher-order unification with dependent function types
• Termination of rewriting in the Calculus of Constructions
• Superposition for full higher-order logic
• Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• A framework for defining logics
• On theories with a combinatorial definition of 'equivalence'
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Higher-order rewrite systems and their confluence
• Proving and applying program transformations expressed with second-order patterns
• Title not available (Why is that?)
• The foundation of a generic theorem prover
• Towards a domain theory for termination proofs

Cited In (4)

• Title not available (Why is that?)
• Higher-order subtyping
• Superposition with datatypes and codatatypes
• Explicit contexts in LF (extended abstract)

Uses Software

• Elf

This page was built for publication: Higher-order superposition for dependent types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055856)