Baumgartner, Peter; Schmidt, Renate A. Blocking and other enhancements for bottom-up model generation methods. (English) Zbl 1468.68279 J. Autom. Reasoning 64, No. 2, 197-251 (2020). MSC: 68V15 03B35 03B70 PDFBibTeX XMLCite \textit{P. Baumgartner} and \textit{R. A. Schmidt}, J. Autom. Reasoning 64, No. 2, 197--251 (2020; Zbl 1468.68279) Full Text: DOI
Bonacina, Maria Paola; Plaisted, David A. Semantically-guided goal-sensitive reasoning: inference system and completeness. (English) Zbl 1437.68189 J. Autom. Reasoning 59, No. 2, 165-218 (2017). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{M. P. Bonacina} and \textit{D. A. Plaisted}, J. Autom. Reasoning 59, No. 2, 165--218 (2017; Zbl 1437.68189) Full Text: DOI
Kowalski, Robert; Sadri, Fariba Programming in logic without logic programming. (English) Zbl 1379.68095 Theory Pract. Log. Program. 16, No. 3, 269-295 (2016). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{R. Kowalski} and \textit{F. Sadri}, Theory Pract. Log. Program. 16, No. 3, 269--295 (2016; Zbl 1379.68095) Full Text: DOI arXiv
Plaisted, David A. History and prospects for first-order automated deduction. (English) Zbl 1465.03055 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 3-28 (2015). MSC: 03B35 03-03 68-03 68V15 PDFBibTeX XMLCite \textit{D. A. Plaisted}, Lect. Notes Comput. Sci. 9195, 3--28 (2015; Zbl 1465.03055) Full Text: DOI
Zhang, Hantao; Zhang, Jian MACE4 and SEM: a comparison of finite model generators. (English) Zbl 1383.68083 Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 101-130 (2013). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{H. Zhang} and \textit{J. Zhang}, Lect. Notes Comput. Sci. 7788, 101--130 (2013; Zbl 1383.68083) Full Text: DOI
Hillenbrand, Thomas; Weidenbach, Christoph Superposition for bounded domains. (English) Zbl 1383.03018 Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 68-100 (2013). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{T. Hillenbrand} and \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 7788, 68--100 (2013; Zbl 1383.03018) Full Text: DOI
Baumgartner, Peter; Furbach, Ulrich; Pelzer, Björn The hyper tableaux calculus with equality and an application to finite model computation. (English) Zbl 1193.03025 J. Log. Comput. 20, No. 1, 77-109 (2010). Reviewer: Nail Zamov (Kazan) MSC: 03B35 68Q15 68T15 PDFBibTeX XMLCite \textit{P. Baumgartner} et al., J. Log. Comput. 20, No. 1, 77--109 (2010; Zbl 1193.03025) Full Text: DOI
Constable, Robert; Moczydłowski, Wojciech Extracting the resolution algorithm from a completeness proof for the propositional calculus. (English) Zbl 1221.03015 Ann. Pure Appl. Logic 161, No. 3, 337-348 (2009). MSC: 03B35 03B05 68T15 PDFBibTeX XMLCite \textit{R. Constable} and \textit{W. Moczydłowski}, Ann. Pure Appl. Logic 161, No. 3, 337--348 (2009; Zbl 1221.03015) Full Text: DOI Link
Baumgartner, Peter; Tinelli, Cesare The model evolution calculus as a first-order DPLL method. (English) Zbl 1182.03034 Artif. Intell. 172, No. 4-5, 591-632 (2008). MSC: 03B35 68T15 68T20 PDFBibTeX XMLCite \textit{P. Baumgartner} and \textit{C. Tinelli}, Artif. Intell. 172, No. 4--5, 591--632 (2008; Zbl 1182.03034) Full Text: DOI
Near, Joseph P.; Byrd, William E.; Friedman, Daniel P. \(\alpha\)leanTAP: a declarative theorem prover for first-order classical logic. (English) Zbl 1183.68561 Garcia de la Banda, Maria (ed.) et al., Logic programming. 24th international conference, ICLP 2008, Udine, Italy, December 9–13 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-89981-5/pbk). Lecture Notes in Computer Science 5366, 238-252 (2008). MSC: 68T15 03B10 PDFBibTeX XMLCite \textit{J. P. Near} et al., Lect. Notes Comput. Sci. 5366, 238--252 (2008; Zbl 1183.68561) Full Text: DOI
Letz, Reinhold; Stenz, Gernot The disconnection tableau calculus. (English) Zbl 1121.03022 J. Autom. Reasoning 38, No. 1-3, 79-126 (2007). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{R. Letz} and \textit{G. Stenz}, J. Autom. Reasoning 38, No. 1--3, 79--126 (2007; Zbl 1121.03022) Full Text: DOI
Baumgartner, Peter; Schmidt, Renate A. Blocking and other enhancements for bottom-up model generation methods. (English) Zbl 1222.68357 Furbach, Ulrich (ed.) et al., Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37187-8/pbk). Lecture Notes in Computer Science 4130. Lecture Notes in Artificial Intelligence, 125-139 (2006). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{P. Baumgartner} and \textit{R. A. Schmidt}, Lect. Notes Comput. Sci. 4130, 125--139 (2006; Zbl 1222.68357) Full Text: DOI arXiv
Eiter, Thomas; Gottlob, Georg Reasoning under minimal upper bounds in propositional logic. (English) Zbl 1142.68532 Theor. Comput. Sci. 369, No. 1-3, 82-115 (2006). MSC: 68T27 03B05 03B60 68T30 PDFBibTeX XMLCite \textit{T. Eiter} and \textit{G. Gottlob}, Theor. Comput. Sci. 369, No. 1--3, 82--115 (2006; Zbl 1142.68532) Full Text: DOI
Bezem, Marc; Coquand, Thierry Automating coherent logic. (English) Zbl 1143.03332 Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 246-260 (2005). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{M. Bezem} and \textit{T. Coquand}, Lect. Notes Comput. Sci. 3835, 246--260 (2005; Zbl 1143.03332) Full Text: DOI
Peltier, N. Some techniques for proving termination of the hyperresolution calculus. (English) Zbl 1112.03012 J. Autom. Reasoning 35, No. 4, 391-427 (2005). MSC: 03B35 03B25 PDFBibTeX XMLCite \textit{N. Peltier}, J. Autom. Reasoning 35, No. 4, 391--427 (2005; Zbl 1112.03012) Full Text: DOI
Miller, Swaha; Plaisted, David A. The space efficiency of OSHL. (English) Zbl 1142.03330 Beckert, Bernhard (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2005, Koblenz, Germany, September 14–17, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28931-3/pbk). Lecture Notes in Computer Science 3702. Lecture Notes in Artificial Intelligence, 217-230 (2005). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{S. Miller} and \textit{D. A. Plaisted}, Lect. Notes Comput. Sci. 3702, 217--230 (2005; Zbl 1142.03330) Full Text: DOI
Hustadt, Ullrich; Motik, Boris; Sattler, Ulrike A decomposition rule for decision procedures by resolution-based calculi. (English) Zbl 1109.03009 Baader, Franz (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture Notes in Artificial Intelligence, 21-35 (2005). MSC: 03B35 PDFBibTeX XMLCite \textit{U. Hustadt} et al., Lect. Notes Comput. Sci. 3452, 21--35 (2005; Zbl 1109.03009) Full Text: DOI
Peltier, N. Representing and building models for decidable subclasses of equational clausal logic. (English) Zbl 1105.03017 J. Autom. Reasoning 33, No. 2, 133-170 (2004). MSC: 03B35 03B25 PDFBibTeX XMLCite \textit{N. Peltier}, J. Autom. Reasoning 33, No. 2, 133--170 (2004; Zbl 1105.03017) Full Text: DOI
Peltier, Nicolas A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract). (English) Zbl 1261.68105 Dahn, Ingo (ed.) et al., FTP’2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP’03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 86, No. 1, 91-104 (2003). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{N. Peltier}, Electron. Notes Theor. Comput. Sci. 86, No. 1, 91--104 (2003; Zbl 1261.68105) Full Text: DOI
Plaisted, David A.; Yahya, Adnan A relevance restriction strategy for automated deduction. (English) Zbl 1079.68093 Artif. Intell. 144, No. 1-2, 59-93 (2003). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{D. A. Plaisted} and \textit{A. Yahya}, Artif. Intell. 144, No. 1--2, 59--93 (2003; Zbl 1079.68093) Full Text: DOI
Peltier, Nicolas Model building with ordered resolution: Extracting models from saturated clause sets. (English) Zbl 1019.03008 J. Symb. Comput. 36, No. 1-2, 5-48 (2003). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{N. Peltier}, J. Symb. Comput. 36, No. 1--2, 5--48 (2003; Zbl 1019.03008) Full Text: DOI
Petermann, Uwe A confluent theory connection calculus. (English) Zbl 1016.03010 Egly, Uwe (ed.) et al., Automated reasoning with analytic tableaux and related methods. 11th international conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 - August 1, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2381, 221-234 (2002). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{U. Petermann}, Lect. Notes Comput. Sci. 2381, 221--234 (2002; Zbl 1016.03010) Full Text: Link
Dix, Jürgen; Furbach, Ulrich; Niemelä, Ilkka Nonmonotonic reasoning: Towards efficient calculi and implementations. (English) Zbl 0991.03036 Robinson, Alan (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier. 1241-1354 (2001). Reviewer: A.Nabebin (Moskva) MSC: 03B70 03B60 68T27 68N17 03B35 68T15 PDFBibTeX XMLCite \textit{J. Dix} et al., in: Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier; Cambridge, MA: MIT Press. 1241--1354 (2001; Zbl 0991.03036)
Schütz, Heribert; Geisler, Tim Efficient model generation through compilation. (English) Zbl 1045.68605 Inf. Comput. 162, No. 1-2, 138-157 (2000). MSC: 68T15 03B35 68N20 PDFBibTeX XMLCite \textit{H. Schütz} and \textit{T. Geisler}, Inf. Comput. 162, No. 1--2, 138--157 (2000; Zbl 1045.68605) Full Text: DOI
Caferra, Ricardo; Peltier, Nicolas Combining enumeration and deductive techniques in order to increase the class of constructible infinite models. (English) Zbl 0965.03012 J. Symb. Comput. 29, No. 2, 177-211 (2000). MSC: 03B35 03B25 68T15 PDFBibTeX XMLCite \textit{R. Caferra} and \textit{N. Peltier}, J. Symb. Comput. 29, No. 2, 177--211 (2000; Zbl 0965.03012) Full Text: DOI Link
Plaisted, David A.; Zhu, Yunshan Ordered semantic hyper-linking. (English) Zbl 0959.68115 J. Autom. Reasoning 25, No. 3, 167-217 (2000). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{D. A. Plaisted} and \textit{Y. Zhu}, J. Autom. Reasoning 25, No. 3, 167--217 (2000; Zbl 0959.68115) Full Text: DOI
Bry, François; Yahya, Adnan Positive unit hyperresolution tableaux and their application to minimal model generation. (English) Zbl 0960.03006 J. Autom. Reasoning 25, No. 1, 35-82 (2000). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{F. Bry} and \textit{A. Yahya}, J. Autom. Reasoning 25, No. 1, 35--82 (2000; Zbl 0960.03006) Full Text: DOI
Weidenbach, Christoph Towards an automatic analysis of security protocols in first-order logic. (English) Zbl 1038.94548 Ganzinger, Harald (ed.), Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7–10, 1999. Proceedings. Berlin: Springer (ISBN 3-540-66222-7). Lect. Notes Comput. Sci. 1632, 314-328 (1999). MSC: 94A60 68T15 03B35 PDFBibTeX XMLCite \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 1632, 314--328 (1999; Zbl 1038.94548)
Bry, François; Torge, Sunna A deduction method complete for refutation and finite satisfiability. (English) Zbl 0928.03031 Dix, Jürgen (ed.) et al., Logics in artificial intelligence. European workshop, JELIA ’98. Dagstuhl, Germany, October 12–15, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1489, 122-138 (1998). MSC: 03B70 68T27 03B35 PDFBibTeX XMLCite \textit{F. Bry} and \textit{S. Torge}, Lect. Notes Comput. Sci. 1489, 122--138 (1998; Zbl 0928.03031)
Peltier, Nicolas A new method for automated finite model building exploiting failures and symmetries. (English) Zbl 0904.68155 J. Log. Comput. 8, No. 4, 511-543 (1998). MSC: 68T15 03C13 PDFBibTeX XMLCite \textit{N. Peltier}, J. Log. Comput. 8, No. 4, 511--543 (1998; Zbl 0904.68155) Full Text: DOI Link
Ganzinger, Harald; Meyer, Christoph; Weidenbach, Christoph Soft typing for ordered resolution. (English) Zbl 1430.68407 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, 321-335 (1997). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{H. Ganzinger} et al., Lect. Notes Comput. Sci. 1249, 321--335 (1997; Zbl 1430.68407) Full Text: DOI
Cryan, Mary; Ramsay, Allan Constructing a normal form for property theory. (English) Zbl 1430.68396 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, 237-251 (1997). MSC: 68V15 03B35 03B65 PDFBibTeX XMLCite \textit{M. Cryan} and \textit{A. Ramsay}, Lect. Notes Comput. Sci. 1249, 237--251 (1997; Zbl 1430.68396) Full Text: DOI
Hasegawa, Ryuzo; Inoue, Katsumi; Ohta, Yoshihiko; Koshimura, Miyuki Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving. (English) Zbl 1430.68410 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, 176-190 (1997). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{R. Hasegawa} et al., Lect. Notes Comput. Sci. 1249, 176--190 (1997; Zbl 1430.68410) Full Text: DOI
Peltier, Nicolas Simplifying and generalizing formulae in tableaux. Pruning the search space and building models. (English) Zbl 1412.68253 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, 313-327 (1997). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{N. Peltier}, Lect. Notes Comput. Sci. 1227, 313--327 (1997; Zbl 1412.68253) Full Text: DOI
Baumgartner, Peter; Fröhlich, Peter; Furbach, Ulrich; Nejdl, Wolfgang Tableaux for diagnosis applications. (English) Zbl 1412.68206 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, 76-90 (1997). MSC: 68T15 03B35 68Q60 PDFBibTeX XMLCite \textit{P. Baumgartner} et al., Lect. Notes Comput. Sci. 1227, 76--90 (1997; Zbl 1412.68206) Full Text: DOI
Baumgartner, Peter; Furbach, Ulrich; Stolzenburg, Frieder Computing answers with model elimination. (English) Zbl 1017.03505 Artif. Intell. 90, No. 1-2, 135-176 (1997). MSC: 03B35 68T15 68N17 PDFBibTeX XMLCite \textit{P. Baumgartner} et al., Artif. Intell. 90, No. 1--2, 135--176 (1997; Zbl 1017.03505) Full Text: DOI
Fermüller, Christian; Leitsch, Alexander Hyperresolution and automated model building. (English) Zbl 0861.68086 J. Log. Comput. 6, No. 2, 173-203 (1996). Reviewer: L.State (Bucureşti) MSC: 68T15 68T27 03B35 PDFBibTeX XMLCite \textit{C. Fermüller} and \textit{A. Leitsch}, J. Log. Comput. 6, No. 2, 173--203 (1996; Zbl 0861.68086) Full Text: DOI
Baumgartner, Peter; Furbach, Ulrich; Niemelä, Ilkka Hyper tableaux. (English) Zbl 1427.03031 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, 1-17 (1996). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{P. Baumgartner} et al., Lect. Notes Comput. Sci. 1126, 1--17 (1996; Zbl 1427.03031) Full Text: DOI
Zhang, Jian; Zhang, Hantao System description – generating models by SEM. (English) Zbl 1412.68268 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, 308-312 (1996). MSC: 68T15 03C13 PDFBibTeX XMLCite \textit{J. Zhang} and \textit{H. Zhang}, Lect. Notes Comput. Sci. 1104, 308--312 (1996; Zbl 1412.68268) Full Text: DOI
Niemelä, Ilkka A tableau calculus for minimal model reasoning. (English) Zbl 1412.68247 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, 278-294 (1996). MSC: 68T15 03B35 68T27 PDFBibTeX XMLCite \textit{I. Niemelä}, Lect. Notes Comput. Sci. 1071, 278--294 (1996; Zbl 1412.68247) Full Text: DOI
Bry, François; Yahya, Adnan Minimal model generation with positive unit hyper-resolution tableaux. (English) Zbl 1412.68212 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, 143-159 (1996). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{F. Bry} and \textit{A. Yahya}, Lect. Notes Comput. Sci. 1071, 143--159 (1996; Zbl 1412.68212) Full Text: DOI
Kowalski, Robert Logic without model theory. (English) Zbl 0820.03012 Gabbay, D. M. (ed.), What is a logical system? Oxford: Oxford University Press. Stud. Log. Comput. 4, 35-71 (1994). Reviewer: D.Makinson (Ville d’Avray) MSC: 03B60 68T35 68T30 PDFBibTeX XMLCite \textit{R. Kowalski}, Stud. Log. Comput. 4, 35--71 (1994; Zbl 0820.03012)
Stickel, Mark E. Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction. (English) Zbl 0819.68113 J. Autom. Reasoning 13, No. 2, 189-210 (1994). MSC: 68T15 03B35 68T27 PDFBibTeX XMLCite \textit{M. E. Stickel}, J. Autom. Reasoning 13, No. 2, 189--210 (1994; Zbl 0819.68113) Full Text: DOI
Hähnle, Reiner Short conjunctive normal forms in finitely valued logics. (English) Zbl 0818.03003 J. Log. Comput. 4, No. 6, 905-927 (1994). Reviewer: D.Mundici (Milano) MSC: 03B35 03B50 03G20 68T15 PDFBibTeX XMLCite \textit{R. Hähnle}, J. Log. Comput. 4, No. 6, 905--927 (1994; Zbl 0818.03003) Full Text: DOI
Zhang, Jian Problems on the generation of finite models. (English) Zbl 1433.68573 Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 753-757 (1994). MSC: 68V15 03B40 03C13 PDFBibTeX XMLCite \textit{J. Zhang}, Lect. Notes Comput. Sci. 814, 753--757 (1994; Zbl 1433.68573) Full Text: DOI
Goubault, Jean Proving with BDDs and control of information. (English) Zbl 1433.68548 Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 499-513 (1994). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{J. Goubault}, Lect. Notes Comput. Sci. 814, 499--513 (1994; Zbl 1433.68548) Full Text: DOI
Chu, Heng; Plaisted, David A. Semantically guided first-order theorem proving using hyper-linking. (English) Zbl 1433.68540 Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 192-206 (1994). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{H. Chu} and \textit{D. A. Plaisted}, Lect. Notes Comput. Sci. 814, 192--206 (1994; Zbl 1433.68540) Full Text: DOI
Slaney, John The crisis in finite mathematics: automated reasoning as cause and cure. (English) Zbl 1433.68566 Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 1-13 (1994). MSC: 68V15 03B35 20N05 PDFBibTeX XMLCite \textit{J. Slaney}, Lect. Notes Comput. Sci. 814, 1--13 (1994; Zbl 1433.68566) Full Text: DOI
Hähnle, Reiner Automated deduction in multiple-valued logics. (English) Zbl 0798.03010 International Series of Monographs on Computer Science. 10. Oxford: Clarendon Press. ix, 172 p. £30.00 /hc (1993). Reviewer: N.Curteanu (Iaşi) MSC: 03B35 68T15 03-02 03B50 68-02 PDFBibTeX XMLCite \textit{R. Hähnle}, Automated deduction in multiple-valued logics. Oxford: Clarendon Press (1993; Zbl 0798.03010)
Fermüller, Christian G.; Leitsch, Alexander Model building by resolution. (English) Zbl 0788.68128 Börger, Egon (ed.) et al., Computer science logic. 6th workshop, CSL ’92, San Miniato, Italy, September 28 - October 2, 1992. Selected papers. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 702, 134-148 (1993). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{C. G. Fermüller} and \textit{A. Leitsch}, Lect. Notes Comput. Sci. 702, 134--148 (1993; Zbl 0788.68128)
McCune, William; Wos, Larry Experiments in automated deduction with condensed detachment. (English) Zbl 0925.68402 Kapur, D. (ed.), Automated deduction - CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15–18, 1992. Berlin: Springer. Lect. Notes Comput. Sci. 607, 209-223 (1992). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{W. McCune} and \textit{L. Wos}, Lect. Notes Comput. Sci. 607, 209--223 (1992; Zbl 0925.68402)
Inoue, Katsumi; Koshimura, Miyuki; Hasegawa, Ryuzo Embedding negation as failure into a model generation theorem prover. (English) Zbl 0925.68417 Kapur, D. (ed.), Automated deduction - CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15–18, 1992. Berlin: Springer. Lect. Notes Comput. Sci. 607, 400-415 (1992). MSC: 68T27 03B35 68N17 68T15 PDFBibTeX XMLCite \textit{K. Inoue} et al., Lect. Notes Comput. Sci. 607, 400--415 (1992; Zbl 0925.68417)