×

zbMATH — the first resource for mathematics

Boolean unification - the story so far. (English) Zbl 0682.68093
From the authors’ introduction: “The most important result is that Boolean unification is unitary, that is either an equation has no solution or there is a single most general unifier (in the sequel: mgu). We present two different unification algorithms, one due to Boole and the other to Löwenheim”.
Reviewer: Reviewer (Berlin)

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q65 Abstract data types; algebraic specification
68W30 Symbolic computation and algebraic computation
Software:
REVE
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Boole, G., (), 1847. Reprinted 1948, B. Blackwell
[2] Boudet, A.; Jouannaud, J.-P.; Schmidt-Schauß, M., Unification in free extensions of Boolean rings and abelian groups, (), 121-131
[3] Boyer, R.S.; Moore, J.S., The sharing of structure in theorem proving programs, () · Zbl 0249.68032
[4] Bryant, R.E., Graph-based algorithms for Boolean function manipulation, IEEE trans. on computers, 35, 8, 677-691, (1986) · Zbl 0593.94022
[5] Büttner, W., Unification in finite algebras is unitary(?), (), 368-377
[6] Büttner, W.; Simonis, H., Embedding Boolean expressions into logic programming, Jsc, 4, 191-205, (1987) · Zbl 0641.68148
[7] Davis, M.; Putnam, H., A computing procedure for quantification theory, Jacm, 7, 201-215, (1960) · Zbl 0212.34203
[8] Garey, M.R.; Johnson, D.S., ()
[9] Herbrand, J., Investigations in proof theory, (), 44-202
[10] Herold, A., Combination of unification algorithms, (), 450-469
[11] Hsiang, J., Refutational theorem proving using term-rewriting systems, Artificial intelligence, 25, (1985) · Zbl 0558.68072
[12] Hsiang, J.; Dershowitz, N., Rewrite rules for clausal and non-clausal theorem proving, (), 431-446
[13] Kapur, D.; Narendran, P., An equational approach to theorem proving in the first order predicate calculus, () · Zbl 0535.68012
[14] Lescanne, P., REVE a rewrite rule laboratory, (), 696-697
[15] Löwenheim, L., Über das auflösungsproblem im logischen klassenkalkül, Sitzungsber. berl. math. gesell., 7, 89-94, (1908) · JFM 39.0089.03
[16] Martin, U.; Nipkow, T., Unification in Boolean rings, (), 506-513
[17] Martin, U.; Nipkow, T., Unification in Boolean rings, Journal of automated reasoning, 4, 381-396, (1989) · Zbl 0659.68111
[18] Monk, J.D., ()
[19] Nipkow, T., Unification in primal algebras, (), 117-131
[20] Nipkow, T., Unification in primal algebras, their powers, and their varieties, (1988), Submitted for publication
[21] Robinson, J.A., A machine oriented logic based on the resolution principle, Jacm, 12, 23-41, (1965) · Zbl 0139.12303
[22] Rudeanu, S., ()
[23] Schmidt-Schauß, M., Unification in a combination of arbitrary disjoint equational theories, (), 378-396
[24] Schröder, E., Vorlesungen über die algebra der logic. (Leipzig, Vol 1, (1890), 1890, Vol 2, 1891, 1905; Vol 3, 1895), Reprint 1966, (Chelsea, Bronx NY) · JFM 22.0073.02
[25] Siekmann, J.H., Universal unification, () · Zbl 0704.68096
[26] Stone, M.H., The theory of representation for Boolean algebras, Trans. amer. math. soc., 40, 37-111, (1936) · Zbl 0014.34002
[27] Tidén, E., Unification in combinations of collapse-free theories with disjoint sets of function symbols, (), 431-449
[28] Van Gelder, A., A satisfiability test for non-clausal propositional calculus, () · Zbl 0546.68074
[29] Vitter, J.S.; Simons, R.A., New classes for parallel complexity: A study of unification and other complete problems for P, IEEE transactions on computers, 403-418, (1986) · Zbl 0613.68023
[30] Yelick, K., Unification in combinations of collapse-free regular theories, Jsc, 3, 153-181, (1987) · Zbl 0638.68105
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.