### Abstract

Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.

Original language | English |
---|---|

Title of host publication | Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings |

Editors | Andrei Voronkov, Michel Parigot |

Publisher | Springer Verlag |

Pages | 96-113 |

Number of pages | 18 |

ISBN (Print) | 3540412859, 9783540412854 |

Publication status | Published - Jan 1 2000 |

Event | 7th International Conference on Logic for Programming and Automated Reasoning, LPAR 2000 - Reunion Island, France Duration: Nov 6 2000 → Nov 10 2000 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 1955 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 7th International Conference on Logic for Programming and Automated Reasoning, LPAR 2000 |
---|---|

Country | France |

City | Reunion Island |

Period | 11/6/00 → 11/10/00 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings*(pp. 96-113). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1955). Springer Verlag.

**Proof simplification for model generation and its applications.** / Koshimura, Miyuki; Hasegawa, Ryuzo.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1955, Springer Verlag, pp. 96-113, 7th International Conference on Logic for Programming and Automated Reasoning, LPAR 2000, Reunion Island, France, 11/6/00.

}

TY - GEN

T1 - Proof simplification for model generation and its applications

AU - Koshimura, Miyuki

AU - Hasegawa, Ryuzo

PY - 2000/1/1

Y1 - 2000/1/1

N2 - Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.

AB - Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.

UR - http://www.scopus.com/inward/record.url?scp=84956866046&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84956866046&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:84956866046

SN - 3540412859

SN - 9783540412854

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 96

EP - 113

BT - Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings

A2 - Voronkov, Andrei

A2 - Parigot, Michel

PB - Springer Verlag

ER -