The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction

QR Code

The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction

Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called...

Full description

Bibliographic Details
Main Authors:	Dennis, Louise Abigail, Bundy, Alan, Green, Ian
Format:	Article
Published:	Kluwer 2000
Online Access:	https://eprints.nottingham.ac.uk/343/

Similar Items

Using a Generalisation Critic to find Bisimulations for Coinductive Proofs
by: Dennis, Louise Abigail, et al.
Published: (1999)

A Comparison of two Proof Critics: Power vs. Robustness
by: Dennis, Louise Abigail, et al.
Published: (2002)

An Architecture for Proof Planning Systems
by: Dennis, Louise Abigail
Published: (2005)

The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs
by: Dennis, Louise Abigail
Published: (2004)

The coinductive formulation of common knowledge
by: Baston, Colm, et al.
Published: (2018)

What can be learned from failed proofs of non-theorems?
by: Dennis, Louise Abigail, et al.
Published: (2005)

On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner
by: Dennis, Louise Abigail, et al.
Published: (2005)

Using coalgebra and coinduction to define ontology-based multi-agent systems
by: Hadzic, Maja, et al.
Published: (2008)

Failure-proof spatio-temporal composition of sensor cloud services
by: Neiat, A., et al.
Published: (2014)

Future-proofing 'Next Generation' infrastructure assets
by: Love, Peter, et al.
Published: (2018)

Witnessing, resonance, authenticity: further explorations in reflexivity
by: Percy, Ian
Published: (2005)

Integrating SVC and HOL with the PROSPER Toolkit
by: Stevenson, Alan, et al.
Published: (2000)

Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
by: Dennis, Louise Abigail, et al.
Published: (2001)

Burdens of proof and the case for unevenness
by: Aijaz, Imran, et al.
Published: (2013)

The principles of witness immunity
by: Shair Mohamed, Mohd. Akram
Published: (2015)

The Competence and Compellability of Witnesses
by: De Vos, Wouter
Published: (2016)

Student attitudes to plagiarism and collusion within computer science
by: Dennis, Louise Abigail
Published: (2005)

Productivity improvement for furniture industry by using witness simulation software
by: Tee, Chun Teck
Published: (2010)

Interactive proof systems
by: Makarin, Rusydi Hasan, et al.
Published: (2011)

Zero-knowledge-proof
by: Alshaikhli, Imad Fakhri Taha, et al.
Published: (2011)

Error Proofing In Manufacturing.
by: Nadarajah, Sivakumar
Published: (2006)

Error Proofing In Manufacturing
by: Nadarajah, Sivakumar
Published: (2006)

Error Proofing In Manufacturing
by: Nadarajah, Sivakumar
Published: (2006)

Improvement of productivity in low volume production industry layout by using witness simulation software
by: Jaffrey, V., et al.
Published: (2017)

Effects of childhood trauma on cortisol levels in suicide attempters and ideators
by: O'Connor, Daryl B., et al.
Published: (2017)

Major abdominal surgery in Jehovah’s Witnesses
by: Rollins, Katie E., et al.
Published: (2016)

Witnesses / Tengku Ibrahim Tengku Kerema
by: Tengku Kerema, Tengku Ibrahim
Published: (1986)

The 1980s as (an Attempt in) the Decolonialization of Malaysian Art
by: Abdullah, Sarena
Published: (2020)

Association of risk of suicide attempts with methylphenidate treatment
by: Man, Kenneth K.C., et al.
Published: (2017)

Productivity improvement for pusat kesihatan pelajar (PKP) by using witness simulation software
by: Chen, Choy Yuen
Published: (2009)

System Description: Embedding Verification into Microsoft Excel
by: Collins, Graham, et al.
Published: (2000)

Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus
by: Zimmer, Juergen, et al.
Published: (2002)

The NumbersWithNames Program
by: Colton, Simon, et al.
Published: (2002)

Witness preparation in the ICC: an opportunity for principled pragmatism
by: Jackson, John D., et al.
Published: (2015)

EVIDENCE PRODUCED BY CHILD WITNESSES AND THE NEED FOR REFORMS
by: Rahul, Antil
Published: (2023)

Single expert witness and action for professional negligence
by: Mohamed Abdullah, Abu Haniffa
Published: (2002)

Road rage witnesses urged to assist cops
by: Shahrudin, Hani Shamira, et al.
Published: (2017)

Datatype-generic termination proofs
by: Backhouse, Roland, et al.
Published: (2008)

Proof Methods for Corecursive Programs
by: Hutton, Graham, et al.
Published: (2005)

Background of zero-knowledge proof
by: Alshaikhli, Imad Fakhri Taha, et al.
Published: (2011)