An overview of LP, the Larch Prover

DOI10.1007/3-540-51081-8_105zbMath1503.68290OpenAlexW2027329270MaRDI QIDQ5055717

Stephen J. Garland, J. V. Guttag

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-51081-8_105

Mathematics Subject Classification ID

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

Related Items (9)

Rewriting, and equational unification: the higher-order cases ⋮ Modular higher-order E-unification ⋮ A decade of TAPSOFT ⋮ Some experiments with a completion theorem prover ⋮ Combining matching algorithms: The regular case ⋮ Behavioural theories and the proof of behavioural properties ⋮ Algebra and automated deduction ⋮ A semi-algorithm for algebraic implementation proofs ⋮ Combining matching algorithms: The regular case

Uses Software

• LARCH

Cites Work

• Orderings for term-rewriting systems
• Proofs by induction in equational theories with constructors
• A Larch shared language handbook
• Proof by consistency
• Unification in combinations of collapse-free regular theories
• The foundation of a generic theorem prover
• Complete Sets of Reductions for Some Equational Theories
• Abstract data types and software validation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An overview of LP, the Larch Prover