@inproceedings{5639acda2d3f47a998da106c224eb6c5,

title = "Proof simplification for model generation and its applications",

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.",

author = "Miyuki Koshimura and Ryuzo Hasegawa",

year = "2000",

month = jan,

day = "1",

language = "English",

isbn = "3540412859",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "96--113",

editor = "Andrei Voronkov and Michel Parigot",

booktitle = "Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings",

address = "Germany",

note = "7th International Conference on Logic for Programming and Automated Reasoning, LPAR 2000 ; Conference date: 06-11-2000 Through 10-11-2000",

}