Connecting many-sorted theories. (English) Zbl 1136.03012

Baader, Franz; Ghilardi, Silvio

J. Symb. Log. 72, No. 2, 535-583 (2007).

The authors develop an interesting and useful approach for merging families of decision procedures in complex logical systems. E.g., good use is made of the well-known Presburger-type procedures/algorithms for arithmetical systems of logic. Indeed, their approach seems to work for merging the several different kinds of algorithms/procedures used to prove the polynomial-time solvability of linear programming problems. They propose a novel scheme for merging many-sorted theories and show under what conditions decidability of the “universal fragment” of the component theories transfers to their combination. If their approach carries over to the situation wherein undecidability of the “universal fragment” of the component theories transfers to their combination then important new results would be available for a better understanding of (1) undecidable theories and (2) recursively enumerable degrees of unsolvability. The authors’ paper will be especially valuable for classical logicians interested in deep problems of artificial intelligence.

Reviewer: Albert A. Mullin (Madison)

MSC:

03B25	Decidability of theories and sets of sentences
03B35	Mechanization of proofs and logical operations
03B45	Modal logic (including the logic of norms)
03D40	Word problems, etc. in computability and recursion theory
68T27	Logic in artificial intelligence

Keywords:

many-sorted theories; automated deduction; artificial intelligence; modal logic; word problems of logic

References:

[1]	First-order categorical logic 611 (1977)
[2]	ACM Transactions on Programming Languages and Systems 1 pp 245–257– (1979)
[3]	Modal logic 53 (2001) · Zbl 0998.03015
[4]	Information and Computation 178 pp 346–390– (2002)
[5]	Proceedings of the 14th International Conference on Automated Deduction 1249 pp 19–33– (1997)
[6]	Journal of Artificial Intelligence Research 16 pp 1–58– (2002)
[7]	DOI: 10.1016/j.ic.2005.05.009 · Zbl 1098.03048
[8]	Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR’04) 3097 pp 183–197– (2004)
[9]	Annals of Pure and Applied Logic 71 pp 131–188– (1995)
[10]	Proceedings of the 20th International Conference on Automated Deduction (CADE-05) 3632 pp 278–294– (2005)
[11]	Proceedings of the 18th International Conference on Automated Deduction (CADE’18) 2392 pp 363–376– (2002)
[12]	Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS 2005) 3717 pp 31–47– (2005)
[13]	Advances in modal logic pp 361–379– (1998)
[14]	Proceedings of the Fourteenth International Conference on Logic Programming pp 331–345– (1997)
[15]	Theoretical Computer Science 290 pp 291–353– (2003)
[16]	Journal of Automated Reasoning 30 pp 1–31– (2003)
[17]	Properties of independently axiomatizable bimodal logics 56 pp 1469–1485– (1991)
[18]	Model theory 42 (1993)
[19]	Sheaves, games and model completions 14 (2002)
[20]	Journal of Automated Reasoning 33 pp 221–249– (2005)
[21]	Logic for computer science: Foundations of automatic theorem proving (1986) · Zbl 0605.03004
[22]	Theoretical Computer Science 294 pp 103–149– (2003)
[23]	Proceedings of the 12th International Conference on Automated Deduction 814 pp 267–281– (1994)
[24]	Model theory (1990)
[25]	Automated theorem proving: After 25 years 29 pp 201–211– (1984)
[26]	Proceedings of the Third International Joint Conference on Automated Reasoning 4130 pp 513–527– (2006)
[27]	Journal of Symbolic Computation 8 pp 51–100– (1989)
[28]	Comptes rendus du congrès de mathématiciens des pays slaves (1929)
[29]	Colloquium Mathematicum 30 pp 15–25– (1974)
[30]	Theoretical Computer Science 12 pp 291–302– (1980)
[31]	Journal of Symbolic Computation 12 pp 633–653– (1991)
[32]	Artificial Intelligence 156 pp 1–73– (2004) · Zbl 1106.68377