TY - GEN
T1 - Higher-order quantification and proof search
AU - Miller, Dale
N1 - Publisher Copyright:
© 2002, Springer-Verlag Berlin Heidelberg.
PY - 2002/1/1
Y1 - 2002/1/1
N2 - Logical equivalence between logic programs that are firstorder logic formulas holds between few logic programs, partly because first-order logic does not allow auxiliary programs and data structures to be hidden. As a result of not having such abstractions, logical equivalence will force these auxiliaries to be present in any equivalence program. Higher-order quantification can be use to hide predicates and function symbols. If such higher-order quantification is restricted so that operationally, only hiding is specified, then the cost of such higher-order quantifiers within proof search can be small: one only needs to deal with adding new eigenvariables and clauses involving such eigenvariables. On the other hand, the specification of hiding via quantification can allow for novel and interesting proofs of logical equivalence between programs. This paper will present several example of how reasoning directly on a logic program can benefit significantly if higher-order quantification is used to provide abstractions.
AB - Logical equivalence between logic programs that are firstorder logic formulas holds between few logic programs, partly because first-order logic does not allow auxiliary programs and data structures to be hidden. As a result of not having such abstractions, logical equivalence will force these auxiliaries to be present in any equivalence program. Higher-order quantification can be use to hide predicates and function symbols. If such higher-order quantification is restricted so that operationally, only hiding is specified, then the cost of such higher-order quantifiers within proof search can be small: one only needs to deal with adding new eigenvariables and clauses involving such eigenvariables. On the other hand, the specification of hiding via quantification can allow for novel and interesting proofs of logical equivalence between programs. This paper will present several example of how reasoning directly on a logic program can benefit significantly if higher-order quantification is used to provide abstractions.
U2 - 10.1007/3-540-45719-4_5
DO - 10.1007/3-540-45719-4_5
M3 - Conference contribution
AN - SCOPUS:84944033085
SN - 9783540441441
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 60
EP - 75
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Kirchner, Helene
A2 - Ringeissen, Christophe
PB - Springer Verlag
T2 - 9th International Conference on Algebraic Methodology and SoftwareTechnology, AMAST 2002
Y2 - 9 September 2002 through 13 September 2002
ER -