Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84–99. Springer, Heidelberg (2009)
Chapter
Google Scholar
Aravindan, C., Baumgartner, P.: Theorem proving techniques for view deletion in databases. J. Symbolic Comput. 29(2), 119–148 (2000)
Article
MathSciNet
MATH
Google Scholar
Arthan, R., Oliva, P.: (Dual) Hoops have unique halving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 165–180. Springer, Heidelberg (2013)
Chapter
Google Scholar
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)
Article
MathSciNet
MATH
Google Scholar
Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. ACM 45(6), 1007–1049 (1998)
Article
MathSciNet
MATH
Google Scholar
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)
Article
MathSciNet
MATH
Google Scholar
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 26, pp. 825–886. IOS Press, Amsterdam (2009)
Google Scholar
Baumgartner, P., Fröhlich, P., Furbach, U., Nejdl, W.: Semantically guided theorem proving for diagnosis applications. In: Proceedings of IJCAI-16, vol. 1, pp. 460–465 (1997)
Google Scholar
Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006)
Article
MATH
Google Scholar
Baumgartner, P., Furbach, U., Niemelä, I.: Hyper tableaux. In: Alferes, J.J., Moniz Pereira, L., Orłowska, E. (eds.) JELIA 1996. LNCS (LNAI), vol. 1126, pp. 1–17. Springer, Heidelberg (1996)
Chapter
Google Scholar
Baumgartner, P., Furbach, U., Pelzer, B.: The hyper tableaux calculus with equality and an application to finite model computation. J. Logic Comput. 20(1), 77–109 (2008)
Article
MathSciNet
MATH
Google Scholar
Baumgartner, P., Pelzer, B., Tinelli, C.: Model evolution calculus with equality - revised and implemented. J. Symbolic Comput. 47(9), 1011–1045 (2012)
Article
MathSciNet
MATH
Google Scholar
Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008)
Article
MathSciNet
MATH
Google Scholar
Baumgartner, P., Waldmann, U.: Superposition and model evolution combined. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 17–34. Springer, Heidelberg (2009)
Chapter
Google Scholar
Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 39–57. Springer, Heidelberg (2013)
Chapter
Google Scholar
Bender, M., Pelzer, B., Schon, C.: System description: E-KRHyper 1.4 – Extensions for unique names and description logic. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 126–134. Springer, Heidelberg (2013)
Chapter
Google Scholar
Bibel, W., Schmitt, P.H. (eds.): Automated Deduction - A Basis for Applications (in 2 volumes). Kluwer Academic Publishers, Dordrecht (1998)
Google Scholar
Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Veloso, M.M., Wooldridge, M.J. (eds.) Artificial Intelligence Today - Recent Trends and Developments. LNCS (LNAI), vol. 1600, pp. 43–84. Springer, Heidelberg (1999)
Chapter
Google Scholar
Bonacina, M.P.: On theorem proving for program checking - Historical perspective and recent developments. In: Fernández, M. (eds.): Proceedings of PPDP-12, pp. 1–11. ACM Press (2010)
Google Scholar
Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symbolic Comput. 45(2), 229–260 (2010)
Article
MathSciNet
MATH
Google Scholar
Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoret. Comput. Sci. 146, 199–242 (1995)
Article
MathSciNet
MATH
Google Scholar
Bonacina, M.P., Hsiang, J.: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. New Gener. Comput. 16(2), 163–200 (1998)
Article
MathSciNet
Google Scholar
Bonacina, M.P., Johansson, M.: Interpolation of ground proofs in automated deduction: a survey. J. Autom. Reasoning 54(4), 353–390 (2015)
Article
MathSciNet
MATH
Google Scholar
Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reasoning 54(1), 69–97 (2015)
Article
MathSciNet
MATH
Google Scholar
Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161–189 (2011)
Article
MathSciNet
MATH
Google Scholar
Bonacina, M.P., Plaisted, D.A.: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of UNIF-28, RISC Technical Reports, pp. 47–54. Johannes Kepler Universität, Linz (2014)
Google Scholar
Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) Proceedings of PAAR-4, EasyChair Proceedings in Computing (EPiC), pp. 25–38 (2015)
Google Scholar
Bonacina, M.P., Plaisted, D.A.: Semantically guided goal-sensitive reasoning: inference system and completeness (2015, in preparation)
Google Scholar
Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reasoning 55(1), 1–29 (2015). doi:10.1007/s10817-015-9334-4
Article
MathSciNet
MATH
Google Scholar
Boy de la Tour, T., Echenim, M.: Permutative rewriting and unification. Inf. Comput. 205(4), 624–650 (2007)
Google Scholar
Chang, C.-L., Lee, R.C.-T.: Symbolic logic and mechanical theorem proving. Academic Press, New York (1973)
MATH
Google Scholar
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Article
MathSciNet
MATH
Google Scholar
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)
Article
MathSciNet
MATH
Google Scholar
de Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)
Article
Google Scholar
de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013)
Chapter
Google Scholar
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier, Amsterdam (1990)
Google Scholar
Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electron. Notes Theoret. Comput. Sci. 238, 103–119 (2009)
Article
MATH
Google Scholar
Fitelson, B.: Gibbard’s collapse theorem for the indicative conditional: an axiomatic approach. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 181–188. Springer, Heidelberg (2013)
Chapter
Google Scholar
Furbach, U., Schon, C.: Semantically guided evolution of \({\cal S}{\cal H}{\cal I}\) ABoxes. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 17–34. Springer, Heidelbeg (2013)
Chapter
Google Scholar
Gallier, J.H., Snyder, W.: Designing unification procedures using transformations: a survey. EATCS Bull. 40, 273–326 (1990)
MATH
Google Scholar
Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 240(10), 1453–1492 (2006)
Article
MathSciNet
MATH
Google Scholar
Ganzinger, H., Waldmann, U.: Theorem proving in cancellative abelian monoids. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE-13. LNCS, vol. 1104, pp. 388–402. Springer, Heidelberg (1996)
Chapter
Google Scholar
Goguen, J., Meseguer, J.: Order-sorted unification. J. Symbolic Comput. 8(4), 383–413 (1989)
Article
MathSciNet
MATH
Google Scholar
Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105(2), 217–273 (1992)
Article
MathSciNet
MATH
Google Scholar
Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)
Chapter
Google Scholar
Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electron. Notes Theoret. Comput. Sci. 290(3), 37–50 (2012)
Article
MATH
Google Scholar
Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151–155. Springer, Heidelberg (2006)
Chapter
Google Scholar
Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559–587 (1991)
Article
MathSciNet
MATH
Google Scholar
Hsiang, J., Rusinowitch, M., Sakai, K.: Complete inference rules for the cancellation laws. In: Proceedings of IJCAI-10, pp. 990–992 (1987)
Google Scholar
Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008)
Chapter
Google Scholar
Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 30–45. Springer, Heidelberg (2010)
Chapter
Google Scholar
Marques-Silva, J.P., Sakallah, K.A.: GRASP: a new search algorithm for satisfiability. In: Proceedings of ICCAD 1996, pp. 220–227 (1997)
Google Scholar
Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 257–321. MIT Press, Cambridge (1991)
Google Scholar
Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)
Article
MathSciNet
MATH
Google Scholar
Jovanović, D., Barrett, C., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of FMCAD-13. ACM and IEEE (2013)
Google Scholar
Kapur, D.: An automated tool for analyzing completeness of equational specifications. In: Proceedings of ISSTA-94, pp. 28–43. ACM (1994)
Google Scholar
Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991)
Article
MathSciNet
MATH
Google Scholar
Lee, S.-J., Plaisted, D.A.: Eliminating duplication with the hyperlinking strategy. J. Autom. Reasoning 9, 25–42 (1992)
Article
MathSciNet
MATH
Google Scholar
Lifschitz, V., Morgenstern, L., Plaisted, D.A.: Knowledge representation and classical logic. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, vol. 1, pp. 3–88. Elsevier, Amsterdam (2008)
Chapter
Google Scholar
Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009)
Article
Google Scholar
McCune, W.W.: OTTER 3.3 reference manual. Technical Report ANL/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne (2003)
Google Scholar
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Blaauw, D., Lavagno, L. (eds.) Proceedings of DAC-39, pp. 530–535 (2001)
Google Scholar
Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201–211. American Mathematical Society, Providence (1983)
Google Scholar
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. 1(2), 245–257 (1979)
Article
MATH
Google Scholar
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)
Article
MathSciNet
MATH
Google Scholar
Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233–264 (1981)
Article
MathSciNet
MATH
Google Scholar
Plaisted, D.A.: Mechanical theorem proving. In: Banerji, R.B. (ed.) Formal Techniques in Artificial Intelligence, pp. 269–320. Elsevier, Amsterdam (1990)
Google Scholar
Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Vol. I: Logical Foundations, pp. 273–364. Oxford University Press, Oxford (1993)
Google Scholar
Plaisted, D.A.: Automated theorem proving. Wiley Interdisciplinary Reviews: Cognitive Science 5(2), 115–128 (2014)
MathSciNet
Google Scholar
Plaisted, D.A., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Friedrich Vieweg & Sohns, Braunschweig (1997)
Book
MATH
Google Scholar
Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reasoning 25, 167–217 (2000)
Article
MathSciNet
MATH
Google Scholar
Plotkin, G.: Building in equational theories. Mach. Intell. 7, 73–90 (1972)
MathSciNet
MATH
Google Scholar
Robinson, G.A., Wos, L.: Paramodulation and theorem proving in first order theories with equality. Mach. Intell. 4, 135–150 (1969)
MathSciNet
MATH
Google Scholar
Robinson, J.A.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965)
MathSciNet
MATH
Google Scholar
Robinson, J.A.: A machine oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Article
MathSciNet
MATH
Google Scholar
Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier and MIT Press, Amsterdam (2001)
MATH
Google Scholar
Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symbolic Comput. 11(1 & 2), 21–50 (1991)
Article
MathSciNet
MATH
Google Scholar
Shearer, R., Motik, B., Horrocks, I.: HermiT: a highly efficient OWL reasoner. In: Ruttenberg, A., Sattler, U., Dolbear, C. (eds.) Proceedings of OWLED-5, vol. 432 of CEUR (2008)
Google Scholar
Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. J. ACM 14(4), 687–697 (1967)
Article
MathSciNet
MATH
Google Scholar
Slaney, J., Lusk, E., McCune, W.: SCOTT: semantically constrained Otter system description. In: Bundy, A. (ed.) CADE-12. LNCS (LNAI), vol. 814, pp. 764–768. Springer, Heidelberg (1994)
Chapter
Google Scholar
Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE-20. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005)
Chapter
Google Scholar
Sofronie-Stokkermans, V.: Hierarchical and modular reasoning in complex theories: the case of local theory extensions. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 47–71. Springer, Heidelberg (2007)
Chapter
Google Scholar
Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4), 1–31, Paper 1 (2008)
Google Scholar
Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoret. Comput. Sci. 208(1–2), 149–177 (1998)
Article
MathSciNet
MATH
Google Scholar
Waldmann, U.: Superposition for divisible torsion-free abelian groups. In: Kirchner, C., Kirchner, H. (eds.) CADE-15. LNCS (LNAI), vol. 1421, pp. 144–159. Springer, Heidelberg (1998)
Chapter
Google Scholar
Wos, L., Carson, D., Robinson, G.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 536–541 (1965)
Article
MathSciNet
MATH
Google Scholar
Zhang, H., Zhang, J.: MACE4 and SEM: a comparison of finite model generators. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 101–130. Springer, Heidelberg (2013)
Chapter
Google Scholar
Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE-18. LNCS (LNAI), vol. 2392, pp. 295–313. Springer, Heidelberg (2002)
Chapter
Google Scholar