Backeman, Peter; Rümmer, Philipp Free variables and theories: revisiting rigid \(E\)-unification. (English) Zbl 1471.68301 Lutz, Carsten (ed.) et al., Frontiers of combining systems. 10th international symposium, FroCoS 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9322, 3-13 (2015). MSC: 68V15 68Q42 PDFBibTeX XMLCite \textit{P. Backeman} and \textit{P. Rümmer}, Lect. Notes Comput. Sci. 9322, 3--13 (2015; Zbl 1471.68301) Full Text: DOI
Giese, Martin Superposition-based equality handling for analytic tableaux. (English) Zbl 1113.68087 J. Autom. Reasoning 38, No. 1-3, 127-153 (2007). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{M. Giese}, J. Autom. Reasoning 38, No. 1--3, 127--153 (2007; Zbl 1113.68087) Full Text: DOI
Levy, Jordi; Veanes, Margus On the undecidability of second-order unification. (English) Zbl 1005.03007 Inf. Comput. 159, No. 1-2, 125-150 (2000). MSC: 03B35 03D35 68Q42 68T15 68W30 PDFBibTeX XMLCite \textit{J. Levy} and \textit{M. Veanes}, Inf. Comput. 159, No. 1--2, 125--150 (2000; Zbl 1005.03007) Full Text: DOI
Degtyarev, A.; Gurevich, Y.; Narendran, P.; Veanes, M.; Voronkov, A. Decidability and complexity of simultaneous rigid E-unification with one variable and related results. (English) Zbl 0944.68103 Theor. Comput. Sci. 243, No. 1-2, 167-184 (2000). MSC: 68Q45 PDFBibTeX XMLCite \textit{A. Degtyarev} et al., Theor. Comput. Sci. 243, No. 1--2, 167--184 (2000; Zbl 0944.68103) Full Text: DOI
Gurevich, Yuri; Veanes, Margus Logic with equality: Partisan corroboration and shifted pairing. (English) Zbl 1004.03036 Inf. Comput. 152, No. 2, 205-235 (1999). MSC: 03D35 03B25 03B35 PDFBibTeX XMLCite \textit{Y. Gurevich} and \textit{M. Veanes}, Inf. Comput. 152, No. 2, 205--235 (1999; Zbl 1004.03036) Full Text: DOI
Gurevich, Yuri; Voronkov, Andrei Monadic simultaneous rigid \(E\)-unification. (English) Zbl 0930.03007 Theor. Comput. Sci. 222, No. 1-2, 133-152 (1999). MSC: 03B35 03B25 03B20 03D40 03D15 68R15 PDFBibTeX XMLCite \textit{Y. Gurevich} and \textit{A. Voronkov}, Theor. Comput. Sci. 222, No. 1--2, 133--152 (1999; Zbl 0930.03007) Full Text: DOI
Voronkov, Andrei Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. (English) Zbl 0937.03020 Theor. Comput. Sci. 224, No. 1-2, 319-352 (1999). MSC: 03B35 03B25 PDFBibTeX XMLCite \textit{A. Voronkov}, Theor. Comput. Sci. 224, No. 1--2, 319--352 (1999; Zbl 0937.03020) Full Text: DOI
Bjørner, Nikolaj S.; Stickel, Mark E.; Uribe, Tomás E. A practical integration of first-order reasoning and decision procedures. (English) Zbl 1430.03037 McCune, William (ed.), Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1249, 101-115 (1997). MSC: 03B35 68Q60 68V15 PDFBibTeX XMLCite \textit{N. S. Bjørner} et al., Lect. Notes Comput. Sci. 1249, 101--115 (1997; Zbl 1430.03037) Full Text: DOI
Komara, Ján; Voda, Paul J. On quasitautologies. (English) Zbl 1415.03024 Galmiche, Didier (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX ’97, Pont-à-Mousson, France, May 13–16, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1227, 231-245 (1997). MSC: 03B35 03B10 03B25 PDFBibTeX XMLCite \textit{J. Komara} and \textit{P. J. Voda}, Lect. Notes Comput. Sci. 1227, 231--245 (1997; Zbl 1415.03024) Full Text: DOI
Gurevich, Yuri; Voronkov, Andrei Monadic simultaneous rigid \(E\)-unification and related problems. (English) Zbl 1401.03037 Degano, Pierpaolo (ed.) et al., Automata, languages and programming. 24th international colloquium, ICALP ’97, Bologna, Italy, July 7–11, 1997. Proceedings. Berlin: Springer-Verlag (ISBN 978-3-540-63165-1/pbk; 978-3-540-69194-5/ebook). Lecture Notes in Computer Science 1256, 154-165 (1997). MSC: 03B35 03B25 03D15 03D40 PDFBibTeX XMLCite \textit{Y. Gurevich} and \textit{A. Voronkov}, Lect. Notes Comput. Sci. 1256, 154--165 (1997; Zbl 1401.03037) Full Text: DOI
Degtyarev, Anatoli; Voronkov, Andrei What you always wanted to know about rigid \(E\)-unification. (English) Zbl 1427.03032 Alferes, José Júlio (ed.) et al., Logics in artificial intelligence. European workshop, JELIA ’96, Évora, Portugal, September 30 – October 3, 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1126, 50-69 (1996). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Degtyarev} and \textit{A. Voronkov}, Lect. Notes Comput. Sci. 1126, 50--69 (1996; Zbl 1427.03032) Full Text: DOI
Voronkov, Andrei Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. (English) Zbl 1415.03011 McRobbie, M. A. (ed.) et al., Automated deduction – CADE-13. 13th international conference on automated deduction, New Brunswick, NJ, USA, July/August 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1104, 32-46 (1996). MSC: 03B20 03B35 PDFBibTeX XMLCite \textit{A. Voronkov}, Lect. Notes Comput. Sci. 1104, 32--46 (1996; Zbl 1415.03011) Full Text: DOI
Beckert, Bernhard; Pape, Christian Incremental theory reasoning methods for semantic tableaux. (English) Zbl 1412.68208 Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 93-109 (1996). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{B. Beckert} and \textit{C. Pape}, Lect. Notes Comput. Sci. 1071, 93--109 (1996; Zbl 1412.68208) Full Text: DOI Link
Becher, Gérard Cyclic connections. (English) Zbl 1415.03017 Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 80-92 (1996). MSC: 03B35 03B44 68T15 PDFBibTeX XMLCite \textit{G. Becher}, Lect. Notes Comput. Sci. 1071, 80--92 (1996; Zbl 1415.03017) Full Text: DOI