### 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 |

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'Proof simplification for model generation and its applications'. Together they form a unique fingerprint.

## Cite this

Koshimura, M., & Hasegawa, R. (2000). Proof simplification for model generation and its applications. In A. Voronkov, & M. Parigot (Eds.),

*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.