Constructor-Based Inductive Theorem Prover
From MaRDI portal
Publication:2848959
DOI10.1007/978-3-642-40206-7_26zbMATH Open1396.68112OpenAlexW133357462MaRDI QIDQ2848959FDOQ2848959
Authors: Daniel Găină, Min Zhang, Yuki Chiba, Yasuhito Arimoto 
Publication date: 13 September 2013
Published in: Algebra and Coalgebra in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-40206-7_26
Recommendations
- Proofs by induction in equational theories with constructors
- scientific article; zbMATH DE number 3891336
- scientific article; zbMATH DE number 3965464
- Constructor-based logics
- scientific article; zbMATH DE number 549978
- Building Theorem Provers
- Proving ground confluence and inductive validity in constructor based equational specifications
- Automatic proofs by induction in theories without constructors
- Focused Inductive Theorem Proving
Cited In (10)
- Stability of termination and sufficient-completeness under pushouts via amalgamation
- Omitting types theorem in hybrid dynamic first-order logic with rigid symbols
- Title not available (Why is that?)
- CITP
- Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
- TIP: tools for inductive provers
- On Automation of OTS/CafeOBJ Method
- From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
- Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
- A Maude environment for CafeOBJ
Uses Software
This page was built for publication: Constructor-Based Inductive Theorem Prover
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848959)
