In this paper, we study an upside-down transformation of a branch in SOL/Connection tableaux and show that SOL/Connection tableaux using the folding-up operation can always accomplish a size-preserving transformation for any branch in any tableau. This fact solves the exponentially-growing size problem caused both by the order-preserving reduction and by an incremental answer computation problem. © Springer-Verlag Berlin Heidelberg 2005.

Iwanuma K., Inoue K., Nabeshima H.

695.pdf    Gửi cho bạn bè

Từ khóa : Problem solving; Theorem proving; Computation problem; SOL/Connection tableaux; Computation theory