Higher-order proof by consistency

DOI10.1007/3-540-62034-6_56zbMATH Open1541.68177MaRDI QIDQ6567778FDOQ6567778

Authors: Henrik Linnestad, Christian Prehofer, Olav Lysne 

Publication date: 5 July 2024

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Isabelle. A generic theorem prover
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Title not available (Why is that?)
• On sufficient-completeness and related properties of term rewriting systems
• Proofs by induction in equational theories with constructors
• Term rewriting induction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proof by consistency in conditional equational theories
• A termination ordering for higher order rewrite systems
• Towards a domain theory for termination proofs
• Title not available (Why is that?)
• Extending Bachmair's method for proof by consistency to the final algebra
• Decidable higher-order unification problems

This page was built for publication: Higher-order proof by consistency

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