Abstrakt. I detta dokument presenterar vi en mekanism för att de ne Names för proof-witnesses av formler och därmed att använda Gentzens cut-rule i logisk programmering. Vi anser att ett program är en uppsättning logiska formler tillsammans med en lista över sådana definitioner. Förekomsten av de ned namnen styr bevissökningen genom att ange när ett fall av cut-rule bör prövas. Genom att använda cut-rule finns det bevis som kan göras dramatiskt kortare. Vi förklarar hur denna idé om att använda cut-rule kan tillämpas på logiken i ärftliga Harrop formler.
Pinto presenterar en mekanism för att definiera namn för proof-witnesses av formler och därmed att använda Gentzens cut-rule i logisk programmering REF.
Cut Formulae and Logic Programming
{'venue': 'ELP', 'journal': None, 'mag_field_of_study': ['Computer Science']}