zbMATH — the first resource for mathematics

Improving the efficiency of reasoning through structure-based reformulation. (English) Zbl 0989.68525
Choueiry, Berthe Y. (ed.) et al., Abstraction, reformulation, and approximation. 4th international symposium, SARA 2000, Horseshoe Bay, TX, USA, July 26-29, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1864, 247-259 (2000).
Summary: We investigate the possibility of improving the efficiency of reasoning through structure-based partitioning of logical theories, combined with partition-based logical reasoning strategies. To this end, we provide algorithms for reasoning with partitions of axioms in first-order and propositional logic. We analyze the computational benefit of our algorithms and detect those parameters of a partitioning that influence the efficiency of computation. These parameters are the number of symbols shared by a pair of partitions, the size of each partition, and the topology of the partitioning. Finally, we provide a greedy algorithm that automatically reformulates a given theory into partitions, exploiting the parameters, that influence the efficieney of computation.
For the entire collection see [Zbl 0941.00037].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T35 Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence