Semi-unification and generalizations of a particularly simple form

1. Baaz, M. Note on the existence of most general semi-unifiers. In Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Krajíček, editors, pp. 20–29. Oxford University Press, 1993.

   Google Scholar 

2. Baaz, M. and P. Pudlák. Kreisel's conjecture for L∃₁. In Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Krajíček, editors, pp. 30–60. Oxford University Press, 1993.

   Google Scholar 

3. Chang, C.-L. and Lee, R.C.-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

   Google Scholar 

4. Farmer, W. M. A unification algorithm for second-order monadic terms. In Ann. Pure Appl. Logic, 39 (1988), 131–174.

   Article  Google Scholar 

5. Krajíček, J. and P. Pudlák. The number of proof lines and the size of proofs in first order logic. Arch. Math. Logic, 27 (1988), 69–84.

   Article  Google Scholar 

6. Kreisel, G. Generalizing Proofs: Implications for Generalizing Theorems Proved in Relatively Few Lines, I. Unpublished manuscript.

   Google Scholar 

7. Kfoury, A., J. Tiuryn, and P. Urzyczyn. The undecidability of the semiunification problem. Information and Computation, 102 (1993), 83–101.

   Article  Google Scholar 

8. Makanin, G. S. The problem of solvability of equations in a free semigroup. Mat. Sb., 103(2), 147–236. English translation in Math. USSR Sb., 32 (1977).

   Google Scholar 

9. Parikh, R. J. Some results on the length of proofs. Trans. Am. Math. Soc., 177 (1973), 29–36.

   Google Scholar 

10. Richardson, D. Sets of theorems with short proofs. J. Symbolic Logic, 39(2), 235–242.

    Google Scholar 

Download references