Wang, Zhenming; Zhu, Jun; Zhao, Ning A new fifth-order finite difference well-balanced multi-resolution WENO scheme for solving shallow water equations. (English) Zbl 1447.65033 Comput. Math. Appl. 80, No. 5, 1387-1404 (2020). MSC: 65M06 65M08 65M12 76M20 76M12 76B15 76L05 35Q35 PDF BibTeX XML Cite \textit{Z. Wang} et al., Comput. Math. Appl. 80, No. 5, 1387--1404 (2020; Zbl 1447.65033) Full Text: DOI
Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas Formally verified approximations of definite integrals. (English) Zbl 07024460 J. Autom. Reasoning 62, No. 2, 281-300 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{A. Mahboubi} et al., J. Autom. Reasoning 62, No. 2, 281--300 (2019; Zbl 07024460) Full Text: DOI
Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C. Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. (English) Zbl 07024052 J. Autom. Reasoning 62, No. 1, 69-91 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{W. Li} et al., J. Autom. Reasoning 62, No. 1, 69--91 (2019; Zbl 07024052) Full Text: DOI
Loveland, Donald; Sabharwal, Ashish; Selman, Bart DPLL: the core of modern satisfiability solvers. (English) Zbl 1439.68026 Omodeo, Eugenio G. (ed.) et al., Martin Davis on computability, computational logic, and mathematical foundations. Cham: Springer. Outst. Contrib. Log. 10, 315-335 (2016). MSC: 68V15 68-03 68R07 68T20 PDF BibTeX XML Cite \textit{D. Loveland} et al., Outst. Contrib. Log. 10, 315--335 (2016; Zbl 1439.68026) Full Text: DOI
Arthan, Robin Denis Now \(f\) is continuous (exercise!). (English) Zbl 1451.68313 J. Formaliz. Reason. 9, No. 1, 33-52 (2016). MSC: 68V15 PDF BibTeX XML Cite \textit{R. D. Arthan}, J. Formaliz. Reason. 9, No. 1, 33--52 (2016; Zbl 1451.68313) Full Text: DOI
Martin-Dorel, Érik; Melquiond, Guillaume Proving tight bounds on univariate expressions with elementary functions in Coq. (English) Zbl 1386.68151 J. Autom. Reasoning 57, No. 3, 187-217 (2016). MSC: 68T15 41A58 65G50 PDF BibTeX XML Cite \textit{É. Martin-Dorel} and \textit{G. Melquiond}, J. Autom. Reasoning 57, No. 3, 187--217 (2016; Zbl 1386.68151) Full Text: DOI
Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš Nested antichains for WS1S. (English) Zbl 1420.68186 Baier, Christel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9035, 658-674 (2015). MSC: 68T15 03B25 03B35 03D05 PDF BibTeX XML Cite \textit{T. Fiedor} et al., Lect. Notes Comput. Sci. 9035, 658--674 (2015; Zbl 1420.68186) Full Text: DOI
Traytel, Dmitriy A coalgebraic decision procedure for WS1S. (English) Zbl 1373.03015 Kreutzer, Stephan (ed.), 24th EACSL annual conference and 29th workshop on computer science logic, CSL’15, Berlin, Germany, September 7–10, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-90-3). LIPIcs – Leibniz International Proceedings in Informatics 41, 487-503 (2015). MSC: 03B25 03D05 68T15 PDF BibTeX XML Cite \textit{D. Traytel}, LIPIcs -- Leibniz Int. Proc. Inform. 41, 487--503 (2015; Zbl 1373.03015) Full Text: DOI
Cerrito, Serenella; David, Amélie; Goranko, Valentin Optimal tableau method for constructive satisfiability testing and model synthesis in the alternating-time temporal logic \(\mathrm{ATL}^+\). (English) Zbl 1367.68246 ACM Trans. Comput. Log. 17, No. 1, Article No. 4, 34 p. (2015). MSC: 68T15 03B44 68Q25 PDF BibTeX XML Cite \textit{S. Cerrito} et al., ACM Trans. Comput. Log. 17, No. 1, Article No. 4, 34 p. (2015; Zbl 1367.68246) Full Text: DOI
Narkawicz, Anthony; Muñoz, César; Dutle, Aaron Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. (English) Zbl 1356.68196 J. Autom. Reasoning 54, No. 4, 285-326 (2015). MSC: 68T15 03B35 PDF BibTeX XML Cite \textit{A. Narkawicz} et al., J. Autom. Reasoning 54, No. 4, 285--326 (2015; Zbl 1356.68196) Full Text: DOI
Mousavi, Hamoon; Shallit, Jeffrey Mechanical proofs of properties of the Tribonacci word. (English) Zbl 1350.68218 Manea, Florin (ed.) et al., Combinatorics on words. 10th international conference, WORDS 2015, Kiel, Germany, September 14–17, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-23659-9/pbk; 978-3-319-23660-5/ebook). Lecture Notes in Computer Science 9304, 170-190 (2015). Reviewer: Francine Blanchet-Sadri (Greensboro) MSC: 68R15 03B25 03B35 11B85 68T15 PDF BibTeX XML Cite \textit{H. Mousavi} and \textit{J. Shallit}, Lect. Notes Comput. Sci. 9304, 170--190 (2015; Zbl 1350.68218) Full Text: DOI arXiv
Gaintzarain, Jose; Lucio, Paqui Logical foundations for more expressive declarative temporal logic programming languages. (English) Zbl 1353.68035 ACM Trans. Comput. Log. 14, No. 4, Article No. 28, 41 p. (2013). MSC: 68N17 03B44 PDF BibTeX XML Cite \textit{J. Gaintzarain} and \textit{P. Lucio}, ACM Trans. Comput. Log. 14, No. 4, Article No. 28, 41 p. (2013; Zbl 1353.68035) Full Text: DOI
Traytel, Dmitriy; Nipkow, Tobias Verified decision procedures for MSO on words based on derivatives of regular expressions. (English) Zbl 1323.68346 Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP ’13, Boston, MA, USA, September 25–27, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2326-0). ACM SIGPLAN Notices 48, No. 9, 3-12 (2013). MSC: 68Q45 03B25 03D05 68N18 68T15 PDF BibTeX XML Cite \textit{D. Traytel} and \textit{T. Nipkow}, in: Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP '13, Boston, MA, USA, September 25--27, 2013. New York, NY: Association for Computing Machinery (ACM). 3--12 (2013; Zbl 1323.68346) Full Text: DOI
Ajspur, Mai; Goranko, Valentin; Shkatov, Dmitry Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge. (English) Zbl 1277.68254 Log. J. IGPL 21, No. 3, 407-437 (2013). MSC: 68T27 03B35 03B42 68T15 68T42 PDF BibTeX XML Cite \textit{M. Ajspur} et al., Log. J. IGPL 21, No. 3, 407--437 (2013; Zbl 1277.68254) Full Text: DOI arXiv
Krauss, Alexander; Nipkow, Tobias Proof Pearl: regular expression equivalence and relation algebra. (English) Zbl 1269.68090 J. Autom. Reasoning 49, No. 1, 95-106 (2012). MSC: 68T15 03G15 68Q45 PDF BibTeX XML Cite \textit{A. Krauss} and \textit{T. Nipkow}, J. Autom. Reasoning 49, No. 1, 95--106 (2012; Zbl 1269.68090) Full Text: DOI
Kruglov, Evgeny; Weidenbach, Christoph Superposition decides the first-order logic fragment over ground theories. (English) Zbl 1262.68160 Math. Comput. Sci. 6, No. 4, 427-456 (2012). MSC: 68T15 03B25 PDF BibTeX XML Cite \textit{E. Kruglov} and \textit{C. Weidenbach}, Math. Comput. Sci. 6, No. 4, 427--456 (2012; Zbl 1262.68160) Full Text: DOI
Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation. (English) Zbl 1253.68291 Log. Methods Comput. Sci. 8, No. 3, Paper No. 16, 29 p. (2012). MSC: 68T15 03B35 68Q42 PDF BibTeX XML Cite \textit{S. Conchon} et al., Log. Methods Comput. Sci. 8, No. 3, Paper No. 16, 29 p. (2012; Zbl 1253.68291) Full Text: DOI
Griggio, Alberto; Le, Thi Thieu Hoa; Sebastiani, Roberto Efficient interpolant generation in satisfiability modulo linear integer arithmetic. (English) Zbl 1256.68138 Log. Methods Comput. Sci. 8, No. 3, Paper No. 3, 31 p. (2012). MSC: 68T15 03C40 68Q60 PDF BibTeX XML Cite \textit{A. Griggio} et al., Log. Methods Comput. Sci. 8, No. 3, Paper No. 3, 31 p. (2012; Zbl 1256.68138) Full Text: DOI
Braibant, Thomas; Pous, Damien Deciding Kleene algebras in Coq. (English) Zbl 1238.68146 Log. Methods Comput. Sci. 8, No. 1, Paper No. 16, 42 p. (2012). MSC: 68T15 68Q45 68Q70 PDF BibTeX XML Cite \textit{T. Braibant} and \textit{D. Pous}, Log. Methods Comput. Sci. 8, No. 1, Paper No. 16, 42 p. (2012; Zbl 1238.68146) Full Text: DOI
Schmidt, Renate A.; Tishkovsky, Dmitry Automated synthesis of tableau calculi. (English) Zbl 1218.03012 Log. Methods Comput. Sci. 7, No. 2, Paper No. 6, 32 p. (2011). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{R. A. Schmidt} and \textit{D. Tishkovsky}, Log. Methods Comput. Sci. 7, No. 2, Paper No. 6, 32 p. (2011; Zbl 1218.03012) Full Text: DOI
Grégoire, Benjamin; Pottier, Loïc; Théry, Laurent Proof certificates for algebra and their application to automatic geometry theorem proving. (English) Zbl 1302.68242 Sturm, Thomas (ed.) et al., Automated deduction in geometry. 7th international workshop, ADG 2008, Shanghai, China, September 22–24, 2008. Revised papers. Berlin: Springer (ISBN 978-3-642-21045-7/pbk). Lecture Notes in Computer Science 6301. Lecture Notes in Artificial Intelligence, 42-59 (2011). MSC: 68T15 13P10 PDF BibTeX XML Cite \textit{B. Grégoire} et al., Lect. Notes Comput. Sci. 6301, 42--59 (2011; Zbl 1302.68242) Full Text: DOI
Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed Canonized rewriting and ground AC completion modulo Shostak theories. (English) Zbl 1315.68219 Abdulla, Parosh Aziz (ed.) et al., Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19834-2/pbk). Lecture Notes in Computer Science 6605, 45-59 (2011). MSC: 68T15 03B25 03B35 03D40 PDF BibTeX XML Cite \textit{S. Conchon} et al., Lect. Notes Comput. Sci. 6605, 45--59 (2011; Zbl 1315.68219) Full Text: DOI
Linh Anh Nguyen; Szałas, Andrzej Checking consistency of an ABox w.r.t. global assumptions in PDL. (English) Zbl 1231.03031 Fundam. Inform. 102, No. 1, 97-113 (2010). MSC: 03B70 03B35 68T15 PDF BibTeX XML Cite \textit{Linh Anh Nguyen} and \textit{A. Szałas}, Fundam. Inform. 102, No. 1, 97--113 (2010; Zbl 1231.03031) Full Text: DOI
Cowen, Robert Generalized Davis-Putnam and satisfiability problems in mathematics. (English) Zbl 1205.03025 Log. J. IGPL 18, No. 3, 456-463 (2010). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{R. Cowen}, Log. J. IGPL 18, No. 3, 456--463 (2010; Zbl 1205.03025) Full Text: DOI
Abate, Pietro; Goré, Rajeev; Widmann, Florian An on-the-fly tableau-based decision procedure for PDL-satisfiability. (English) Zbl 1347.68298 Areces, Carlos (ed.) et al., Proceedings of the 5th workshop on methods for modalities (M4M5 2007), Cachan, France, November 29–30, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 231, 191-209 (2009). MSC: 68T15 03B70 68Q25 PDF BibTeX XML Cite \textit{P. Abate} et al., Electron. Notes Theor. Comput. Sci. 231, 191--209 (2009; Zbl 1347.68298) Full Text: DOI
Wernhard, Christoph Automated deduction for projection elimination. (English) Zbl 1200.68227 DISKI. Dissertationen zur Künstlichen Intelligenz 324. Heidelberg: Akademische Verlagsgesellschaft Aka; Amsterdam: IOS Press (Diss. 2008) (ISBN 978-1-58603-983-7; 978-3-89838-324-0/pbk). x, 273 p. (2009). Reviewer: Ion Iancu (Craiova) MSC: 68T30 68T15 68T27 68-02 PDF BibTeX XML Cite \textit{C. Wernhard}, Automated deduction for projection elimination. Heidelberg: Akademische Verlagsgesellschaft Aka; Amsterdam: IOS Press (Diss. 2008) (2009; Zbl 1200.68227)
Haarslev, Volker; Pai, Hsueh-Ieng; Shiri, Nematollaah A formal framework for description logics with uncertainty. (English) Zbl 1191.68649 Int. J. Approx. Reasoning 50, No. 9, 1399-1415 (2009). MSC: 68T27 68T30 68T15 PDF BibTeX XML Cite \textit{V. Haarslev} et al., Int. J. Approx. Reasoning 50, No. 9, 1399--1415 (2009; Zbl 1191.68649) Full Text: DOI
Thang, Phan Minh; Dung, Phan Minh; Hung, Nguyen Duy Towards a common framework for dialectical proof procedures in abstract argumentation. (English) Zbl 1185.68677 J. Log. Comput. 19, No. 6, 1071-1109 (2009). MSC: 68T27 PDF BibTeX XML Cite \textit{P. M. Thang} et al., J. Log. Comput. 19, No. 6, 1071--1109 (2009; Zbl 1185.68677) Full Text: DOI
Schmidt, Renate A.; Tishkovsky, Dmitry Automated synthesis of tableau calculi. (English) Zbl 1218.03011 Giese, Martin (ed.) et al., Automated reasoning with analytic tableaux and related methods. 18th international conference, TABLEAUX 2009, Oslo, Norway, July 6–10, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02715-4/pbk). Lecture Notes in Computer Science 5607. Lecture Notes in Artificial Intelligence, 310-324 (2009). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{R. A. Schmidt} and \textit{D. Tishkovsky}, Lect. Notes Comput. Sci. 5607, 310--324 (2009; Zbl 1218.03011) Full Text: DOI
Burrieza, A.; Mora, A.; Ojeda-Aciego, M.; Orłowska, E. An implementation of a dual tableaux system for order-of-magnitude qualitative reasoning. (English) Zbl 1191.03008 Int. J. Comput. Math. 86, No. 10-11, 1852-1866 (2009). Reviewer: Viorica Sofronie-Stokkermans (Saarbrücken) MSC: 03B35 03B45 05E10 68T15 PDF BibTeX XML Cite \textit{A. Burrieza} et al., Int. J. Comput. Math. 86, No. 10--11, 1852--1866 (2009; Zbl 1191.03008) Full Text: DOI
Tveretina, Olga; Wesselink, Wieger EufDPLL – a tool to check satisfiability of equality logic formulas. (English) Zbl 1336.68167 Seda, Anthony (ed.) et al., Proceedings of the Irish conference on the mathematical foundations of computer science and information technology (MFCSIT 2006), National University of Ireland, Cork, Ireland, August 1–5, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 225, 405-420 (2009). MSC: 68Q60 03B70 68T15 PDF BibTeX XML Cite \textit{O. Tveretina} and \textit{W. Wesselink}, Electron. Notes Theor. Comput. Sci. 225, 405--420 (2008; Zbl 1336.68167) Full Text: DOI
Sieg, Wilfried; Field, Clinton Automated search for Gödel’s proofs. (English) Zbl 1191.03010 Lupacchini, Rossella (ed.) et al., Deduction, computation, experiment. Exploring the effectiveness of proof. Including papers from the workshop held at the University of Bologna, Bologna, Italy, April 3–4, 2007. Berlin: Springer (ISBN 978-88-470-0783-3/pbk). 117-140 (2008). MSC: 03B35 68T15 68T20 PDF BibTeX XML Cite \textit{W. Sieg} and \textit{C. Field}, in: Deduction, computation, experiment. Exploring the effectiveness of proof. Including papers from the workshop held at the University of Bologna, Bologna, Italy, April 3--4, 2007. Berlin: Springer. 117--140 (2008; Zbl 1191.03010) Full Text: DOI
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 PDF BibTeX XML Cite \textit{P. Baumgartner} and \textit{C. Tinelli}, Artif. Intell. 172, No. 4--5, 591--632 (2008; Zbl 1182.03034) Full Text: DOI
Hustadt, Ullrich; Motik, Boris; Sattler, Ulrike Deciding expressive description logics in the framework of resolution. (English) Zbl 1146.68456 Inf. Comput. 206, No. 5, 579-601 (2008). MSC: 68T20 PDF BibTeX XML Cite \textit{U. Hustadt} et al., Inf. Comput. 206, No. 5, 579--601 (2008; Zbl 1146.68456) Full Text: DOI
Sinz, Carsten Visualizing SAT instances and runs of the DPLL algorithm. (English) Zbl 1129.68502 J. Autom. Reasoning 39, No. 2, 219-243 (2007). MSC: 68T15 68T20 PDF BibTeX XML Cite \textit{C. Sinz}, J. Autom. Reasoning 39, No. 2, 219--243 (2007; Zbl 1129.68502) Full Text: DOI
Badban, Bahareh; Van De Pol, Jaco; Tveretina, Olga; Zantema, Hans Generalizing DPLL and satisfiability for equalities. (English) Zbl 1121.68102 Inf. Comput. 205, No. 8, 1188-1211 (2007). MSC: 68T15 68T20 03B25 03B35 PDF BibTeX XML Cite \textit{B. Badban} et al., Inf. Comput. 205, No. 8, 1188--1211 (2007; Zbl 1121.68102) Full Text: DOI
Aiguier, Marc; Bahrami, Diane Structures for abstract rewriting. (English) Zbl 1125.03011 J. Autom. Reasoning 38, No. 4, 303-351 (2007). MSC: 03B35 68Q42 68T15 PDF BibTeX XML Cite \textit{M. Aiguier} and \textit{D. Bahrami}, J. Autom. Reasoning 38, No. 4, 303--351 (2007; Zbl 1125.03011) Full Text: DOI
Havas, George; Ramsay, Colin On proofs in finitely presented groups. (English) Zbl 1120.20032 Campbell, C.M. (ed.) et al., Groups St. Andrews 2005. Vol. II. Selected papers of the conference, St. Andrews, UK, July 30–August 6, 2005. Cambridge: Cambridge University Press (ISBN 978-0-521-69470-4/pbk). London Mathematical Society Lecture Note Series 340, 457-474 (2007). MSC: 20F05 68T15 20F06 20F10 20-04 68W30 PDF BibTeX XML Cite \textit{G. Havas} and \textit{C. Ramsay}, Lond. Math. Soc. Lect. Note Ser. 340, 457--474 (2007; Zbl 1120.20032)
Mahboubi, Assia Implementing the cylindrical algebraic decomposition within the Coq system. (English) Zbl 1121.03023 Math. Struct. Comput. Sci. 17, No. 1, 99-127 (2007). Reviewer: Nail Zamov (Kazan) MSC: 03B35 68T15 68Q25 68W30 PDF BibTeX XML Cite \textit{A. Mahboubi}, Math. Struct. Comput. Sci. 17, No. 1, 99--127 (2007; Zbl 1121.03023) Full Text: DOI
Lahiri, Shuvendu K.; Qadeer, Shaz Verifying properties of well-founded linked lists. (English) Zbl 1369.68143 Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’06, Charleston, SC, USA, January 11–13, 2006. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-027-2). 115-126 (2006). MSC: 68N30 68P05 68T15 PDF BibTeX XML Cite \textit{S. K. Lahiri} and \textit{S. Qadeer}, in: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '06, Charleston, SC, USA, January 11--13, 2006. New York, NY: Association for Computing Machinery (ACM). 115--126 (2006; Zbl 1369.68143) Full Text: DOI
Sieg, Wilfried; Field, Clinton Automated search for Gödel’s proofs. (English) Zbl 1064.03010 Ann. Pure Appl. Logic 133, No. 1-3, 319-338 (2005). MSC: 03B35 68T15 68T20 PDF BibTeX XML Cite \textit{W. Sieg} and \textit{C. Field}, Ann. Pure Appl. Logic 133, No. 1--3, 319--338 (2005; Zbl 1064.03010) 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 PDF BibTeX XML Cite \textit{N. Peltier}, J. Autom. Reasoning 33, No. 2, 133--170 (2004; Zbl 1105.03017) Full Text: DOI
Nicoreştianu, Felicia Eugenia A numerical method for super-resolution in confocal scanning microscopy. (English) Zbl 1114.78351 Sci. Bull., Ser. A, Appl. Math. Phys., Politeh. Univ. Buchar. 66, No. 2-4, 27-36 (2004). MSC: 78A55 78A70 PDF BibTeX XML Cite \textit{F. E. Nicoreştianu}, Sci. Bull., Ser. A, Appl. Math. Phys., Politeh. Univ. Buchar. 66, No. 2--4, 27--36 (2004; Zbl 1114.78351)
Tveretina, Olga A decision procedure for equality logic with uninterpreted functions. (English) Zbl 1109.68581 Buchberger, Bruno (ed.) et al., Artificial intelligence and symbolic computation. 7th international conference, AISC 2004, Linz, Austria, September 22–24, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23212-5/pbk). Lecture Notes in Computer Science 3249. Lecture Notes in Artificial Intelligence, 66-79 (2004). MSC: 68T15 68T20 PDF BibTeX XML Cite \textit{O. Tveretina}, Lect. Notes Comput. Sci. 3249, 66--79 (2004; Zbl 1109.68581) Full Text: DOI
Ghilardi, Silvio Model-theoretic methods in combined constraint satisfiability. (English) Zbl 1069.03008 J. Autom. Reasoning 33, No. 3-4, 221-249 (2004). Reviewer: Nicolae Ţăndăreanu (Craiova) MSC: 03B35 03B25 03C10 68T15 PDF BibTeX XML Cite \textit{S. Ghilardi}, J. Autom. Reasoning 33, No. 3--4, 221--249 (2004; Zbl 1069.03008) Full Text: DOI
Beckert, Bernhard Depth-first proof search without backtracking for free-variable clausal tableaux. (English) Zbl 1019.03006 J. Symb. Comput. 36, No. 1-2, 117-138 (2003). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{B. Beckert}, J. Symb. Comput. 36, No. 1--2, 117--138 (2003; Zbl 1019.03006) Full Text: DOI
Baader, Franz; Tinelli, Cesare Deciding the word problem in the union of equational theories. (English) Zbl 1049.03032 Inf. Comput. 178, No. 2, 346-390 (2002). MSC: 03D40 03B25 03C05 03B35 68Q42 68T15 PDF BibTeX XML Cite \textit{F. Baader} and \textit{C. Tinelli}, Inf. Comput. 178, No. 2, 346--390 (2002; Zbl 1049.03032) Full Text: DOI
Hustadt, Ullrich; Schmidt, Renate A. Using resolution for testing modal satisfiability and building models. (English) Zbl 1005.03010 J. Autom. Reasoning 28, No. 2, 205-232 (2002). Reviewer: Manuel Ojeda Aciego (Malaga) MSC: 03B35 03B45 68T15 PDF BibTeX XML Cite \textit{U. Hustadt} and \textit{R. A. Schmidt}, J. Autom. Reasoning 28, No. 2, 205--232 (2002; Zbl 1005.03010) Full Text: DOI
Siekmann, Jörg; Wrightson, Graham An open research problem: Strong completeness of R. Kowalski’s connection graph proof procedure. (English) Zbl 0997.03013 Log. J. IGPL 10, No. 1, 85-103 (2002). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{J. Siekmann} and \textit{G. Wrightson}, Log. J. IGPL 10, No. 1, 85--103 (2002; Zbl 0997.03013) Full Text: DOI
Beame, Paul; Karp, Richard; Pitassi, Toniann; Saks, Michael The efficiency of resolution and Davis-Putnam procedures. (English) Zbl 1004.03048 SIAM J. Comput. 31, No. 4, 1048-1075 (2002). MSC: 03F20 03B35 68T15 68T20 68Q25 68Q17 68W40 03D15 PDF BibTeX XML Cite \textit{P. Beame} et al., SIAM J. Comput. 31, No. 4, 1048--1075 (2002; Zbl 1004.03048) Full Text: DOI
Ganzinger, Harald; Hustadt, Ullrich; Meyer, Christoph; Schmidt, Renate A. A resolution-based decision procedure for extensions of K4. (English) Zbl 0993.03017 Zakharyaschev, Michael (ed.) et al., Advances in modal logic. Vol. 2. Selected papers from the 2nd international workshop (AiML’98), Uppsala, Sweden, October 16-18, 1998. Stanford, CA: CSLI Publications. CSLI Lect. Notes. 119, 225-246 (2001). MSC: 03B45 03B25 03B35 PDF BibTeX XML Cite \textit{H. Ganzinger} et al., in: Advances in modal logic. Vol. 2. Selected papers from the 2nd international workshop (AiML'98), Uppsala, Sweden, October 16--18, 1998. Stanford, CA: CSLI Publications. 225--246 (2001; Zbl 0993.03017)
Moukalled, F.; Darwish, M. A high-resolution pressure-based algorithm for fluid flow at all speeds. (English) Zbl 0991.76047 J. Comput. Phys. 168, No. 1, 101-130 (2001). MSC: 76M12 76N15 76D05 PDF BibTeX XML Cite \textit{F. Moukalled} and \textit{M. Darwish}, J. Comput. Phys. 168, No. 1, 101--130 (2001; Zbl 0991.76047) Full Text: DOI
Walther, Christoph; Kolbe, Thomas On terminating lemma speculations. (English) Zbl 1045.68606 Inf. Comput. 162, No. 1-2, 96-116 (2000). MSC: 68T15 PDF BibTeX XML Cite \textit{C. Walther} and \textit{T. Kolbe}, Inf. Comput. 162, No. 1--2, 96--116 (2000; Zbl 1045.68606) Full Text: DOI
Wang, Tie-Chung; Goldberg, Allen Integration of linear arithmetic and goal-oriented resolution for software reasoning. (English) Zbl 1004.68144 Gabbay, Dov M. (ed.) et al., Frontiers of combining systems 2. Selected papers from the 2nd international workshop (FroCoS’98), Amsterdam, Netherlands, October 2-4, 1998. Baldock: Research Studies Press. Stud. Log. Comput. 7, 361-378 (2000). MSC: 68T15 03B35 68Q60 68N30 PDF BibTeX XML Cite \textit{T.-C. Wang} and \textit{A. Goldberg}, in: Frontiers of combining systems 2. Selected papers from the 2nd international workshop (FroCoS'98), Amsterdam, Netherlands, October 2--4, 1998. Baldock: Research Studies Press. 361--378 (2000; Zbl 1004.68144)
Basin, David; Friedrich, Stefan Combining WS1S and HOL. (English) Zbl 0988.03024 Gabbay, Dov M. (ed.) et al., Frontiers of combining systems 2. Selected papers from the 2nd international workshop (FroCoS’98), Amsterdam, Netherlands, October 2-4, 1998. Baldock: Research Studies Press. Stud. Log. Comput. 7, 39-56 (2000). MSC: 03B35 68T15 03B15 PDF BibTeX XML Cite \textit{D. Basin} and \textit{S. Friedrich}, in: Frontiers of combining systems 2. Selected papers from the 2nd international workshop (FroCoS'98), Amsterdam, Netherlands, October 2--4, 1998. Baldock: Research Studies Press. 39--56 (2000; Zbl 0988.03024)
Hustadt, Ullrich; Schmidt, Renate A. Using resolution for testing modal satisfiability and building models. (English) Zbl 0984.03012 Gent, Ian (ed.) et al., SAT2000. Highlights of satisfiability research in the year 2000. 3rd international workshop, September 1998. Amsterdam: IOS Press. Front. Artif. Intell. Appl. 63, 459-483 (2000). Reviewer: U.Schöning (Ulm) MSC: 03B35 03B45 PDF BibTeX XML Cite \textit{U. Hustadt} and \textit{R. A. Schmidt}, Front. Artif. Intell. Appl. 63, 459--483 (2000; Zbl 0984.03012)
Baaz, Matthias; Leitsch, Alexander Cut-elimination and redundancy-elimination by resolution. (English) Zbl 0976.03059 J. Symb. Comput. 29, No. 2, 149-176 (2000). Reviewer: G.Mints (Stanford) MSC: 03F05 03B35 68T15 03B10 PDF BibTeX XML Cite \textit{M. Baaz} and \textit{A. Leitsch}, J. Symb. Comput. 29, No. 2, 149--176 (2000; Zbl 0976.03059) Full Text: DOI
Génisson, Richard; Jégou, Philippe On the relations between SAT and CSP enumerative algorithms. (English) Zbl 0965.03015 Discrete Appl. Math. 107, No. 1-3, 27-40 (2000). MSC: 03B35 68T15 68Q25 PDF BibTeX XML Cite \textit{R. Génisson} and \textit{P. Jégou}, Discrete Appl. Math. 107, No. 1--3, 27--40 (2000; Zbl 0965.03015) Full Text: DOI
Li, Chu Min Equivalency reasoning to solve a class of hard SAT problems. (English) Zbl 1063.68591 Inf. Process. Lett. 76, No. 1-2, 75-81 (2000). MSC: 68Q25 68T15 PDF BibTeX XML Cite \textit{C. M. Li}, Inf. Process. Lett. 76, No. 1--2, 75--81 (2000; Zbl 1063.68591) Full Text: DOI
Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M. Normal forms and proofs in combined modal and temporal logics. (English) Zbl 0964.03011 Kirchner, Hélène (ed.) et al., Frontiers of combining systems. 3rd international workshop, FroCoS 2000, Nancy, France, March 22-24, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1794, 73-87 (2000). Reviewer: Valentin F.Goranko (Johannesburg) MSC: 03B35 03F05 03B45 03B44 PDF BibTeX XML Cite \textit{U. Hustadt} et al., Lect. Notes Comput. Sci. 1794, 73--87 (2000; Zbl 0964.03011)
Leitsch, Alexander Resolution and the decision problem. (English) Zbl 0958.03008 Cantini, Andrea (ed.) et al., Logic and foundations of mathematics. Selected contributed papers of the 10th international congress of logic, methodology and philosophy of science, Florence, August 19-25, 1995. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 280, 249-269 (1999). Reviewer: N.Zamov (Kazan’) MSC: 03B25 03B35 PDF BibTeX XML Cite \textit{A. Leitsch}, Synth. Libr. 280, 249--269 (1999; Zbl 0958.03008)
Kurihara, Masahito; Kondo, Hisashi Completion for multiple reduction orderings. (English) Zbl 0951.68149 J. Autom. Reasoning 23, No. 1, 25-42 (1999). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{M. Kurihara} and \textit{H. Kondo}, J. Autom. Reasoning 23, No. 1, 25--42 (1999; Zbl 0951.68149) Full Text: DOI
Areces, Carlos; de Nivelle, Hans; de Rijke, Maarten Prefixed resolution. A resolution method for modal and description logics. (English) Zbl 0937.03014 Ganzinger, Harald (ed.), Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7-10, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1632, 187-201 (1999). MSC: 03B35 03B45 PDF BibTeX XML Cite \textit{C. Areces} et al., Lect. Notes Comput. Sci. 1632, 187--201 (1999; Zbl 0937.03014)
Stokkermans, Karel A categorical critical-pair completion algorithm. (English) Zbl 0933.18002 J. Symb. Comput. 27, No. 5, 435-477 (1999). Reviewer: C.Calude (Auckland) MSC: 18A99 68W30 68Q42 13P10 PDF BibTeX XML Cite \textit{K. Stokkermans}, J. Symb. Comput. 27, No. 5, 435--477 (1999; Zbl 0933.18002) Full Text: DOI
Bibel, Wolfgang; Brüning, Stefan; Otten, Jens; Rath, Thomas; Schaub, Torsten Compressions and extensions. (English) Zbl 0971.03014 Bibel, Wolfgang (ed.) et al., Automated deduction. A basis for applications. Vol. 1: Foundations, calculi and methods. Dordrecht: Kluwer Academic Publishers; 0-7923-5132-0 (set)). Appl. Log. Ser. 8, 133-190 (1998). Reviewer: Manuel Ojeda Aciego (Malaga) MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{W. Bibel} et al., Appl. Log. Ser. 8, 133--190 (1998; Zbl 0971.03014)
Matsuoka, Satoshi Towards a higher order unification based on proof nets. (English) Zbl 0944.68167 RIMS Kokyuroku 1023, 1-15 (1998). MSC: 68T15 03B35 03F50 PDF BibTeX XML Cite \textit{S. Matsuoka}, RIMS Kokyuroku 1023, 1--15 (1998; Zbl 0944.68167)
Kim, Sang Wu; Kim, Sang Mun Proof procedures for an automated theorem-proving program. (English) Zbl 0937.03018 Kybernetes 27, No. 8-9, 1075-1078 (1998). MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{S. W. Kim} and \textit{S. M. Kim}, Kybernetes 27, No. 8--9, 1075--1078 (1998; Zbl 0937.03018)
de Nivelle, Hans A resolution decision procedure for the guarded fragment. (English) Zbl 0927.03027 Kirchner, Claude (ed.) et al., Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5–10, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1421, 191-204 (1998). MSC: 03B35 03B25 03B45 PDF BibTeX XML Cite \textit{H. de Nivelle}, Lect. Notes Comput. Sci. 1421, 191--204 (1998; Zbl 0927.03027)
Mundici, Daniele; Olivetti, Nicola Resolution and model building in the infinite-valued calculus of Łukasiewicz. (English) Zbl 0921.03013 Theor. Comput. Sci. 200, No. 1-2, 335-366 (1998). Reviewer: N.Zamov (Kazan’) MSC: 03B35 03B50 PDF BibTeX XML Cite \textit{D. Mundici} and \textit{N. Olivetti}, Theor. Comput. Sci. 200, No. 1--2, 335--366 (1998; Zbl 0921.03013) Full Text: DOI
Schmidt, Renate A. Resolution is a decision procedure for many propositional modal logics. (English) Zbl 0913.03019 Kracht, Marcus (ed.) et al., Advances in modal logic. Vol. 1. Selected papers of the 1st AiML conference, Free University of Berlin, Germany, October 1996. Stanford, CA: Center for the Study of Language and Information (CSLI). CSLI Lect. Notes. 87, 189-208 (1998). Reviewer: N.Zamov (Kazan’) MSC: 03B25 03B45 03B35 PDF BibTeX XML Cite \textit{R. A. Schmidt}, in: Advances in modal logic. Vol. 1. Selected papers of the 1st AiML conference, Free University of Berlin, Germany, October 1996. Stanford, CA: Center for the Study of Language and Information (CSLI). 189--208 (1998; Zbl 0913.03019)
Giunchiglia, Fausto; Roveri, Marco; Sebastiani, Roberto A new method for testing decision procedures in modal logics. (English) Zbl 1430.68409 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, 264-267 (1997). MSC: 68V15 03B35 03B45 PDF BibTeX XML Cite \textit{F. Giunchiglia} et al., Lect. Notes Comput. Sci. 1249, 264--267 (1997; Zbl 1430.68409) 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 PDF BibTeX XML Cite \textit{N. S. Bjørner} et al., Lect. Notes Comput. Sci. 1249, 101--115 (1997; Zbl 1430.03037) Full Text: DOI
Straccia, Umberto A sequent calculus for reasoning in four-valued description logics. (English) Zbl 1412.68274 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, 343-357 (1997). MSC: 68T27 03B50 68T15 PDF BibTeX XML Cite \textit{U. Straccia}, Lect. Notes Comput. Sci. 1227, 343--357 (1997; Zbl 1412.68274) 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 PDF BibTeX XML Cite \textit{N. Peltier}, Lect. Notes Comput. Sci. 1227, 313--327 (1997; Zbl 1412.68253) Full Text: DOI
Makarov, Evgeny A proof procedure for hereditary Harrop formulas with free equality. (English) Zbl 0888.03017 Adian, S. (ed.) et al., Logical foundations of computer science. 4th international symposium, LFCS ’97, Yaroslavl, Russia, July 6–12, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1234, 203-213 (1997). MSC: 03B70 68N17 03B35 PDF BibTeX XML Cite \textit{E. Makarov}, Lect. Notes Comput. Sci. 1234, 203--213 (1997; Zbl 0888.03017)
Harao, Masateru Proof discovery in LK system by analogy. (English) Zbl 0899.03012 Shyamasundar, R. K. (ed.) et al., Advances in computing science - ASIAN ’97. 3rd Asian computing science conference, Kathmandu, Nepal, December 9–11, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1345, 197-211 (1997). Reviewer: L.State (Bucureşti) MSC: 03B35 68T15 03B40 PDF BibTeX XML Cite \textit{M. Harao}, Lect. Notes Comput. Sci. 1345, 197--211 (1997; Zbl 0899.03012)
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 PDF BibTeX XML Cite \textit{P. Baumgartner} et al., Lect. Notes Comput. Sci. 1126, 1--17 (1996; Zbl 1427.03031) Full Text: DOI
Rueß, Harald Reflection of formal tactics in a deductive reflection framework. (English) Zbl 1412.68257 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, 628-642 (1996). MSC: 68T15 03B35 PDF BibTeX XML Cite \textit{H. Rueß}, Lect. Notes Comput. Sci. 1104, 628--642 (1996; Zbl 1412.68257) Full Text: DOI
Giunchiglia, Fausto; Sebastiani, Roberto Building decision procedures for modal logics from propositional decision procedures – the case study of modal K. (English) Zbl 1415.03022 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, 583-597 (1996). MSC: 03B35 03B25 03B45 68T15 PDF BibTeX XML Cite \textit{F. Giunchiglia} and \textit{R. Sebastiani}, Lect. Notes Comput. Sci. 1104, 583--597 (1996; Zbl 1415.03022) Full Text: DOI
Cyrluk, David; Lincoln, Patrick; Shankar, Natarajan On Shostak’s decision procedure for combinations of theories. (English) Zbl 1415.03019 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, 463-477 (1996). MSC: 03B35 03B25 03B62 68T15 PDF BibTeX XML Cite \textit{D. Cyrluk} et al., Lect. Notes Comput. Sci. 1104, 463--477 (1996; Zbl 1415.03019) Full Text: DOI
Homeier, Peter V.; Martin, David F. Mechanical verification of mutually recursive procedures. (English) Zbl 1412.68138 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, 201-215 (1996). MSC: 68Q60 68T15 PDF BibTeX XML Cite \textit{P. V. Homeier} and \textit{D. F. Martin}, Lect. Notes Comput. Sci. 1104, 201--215 (1996; Zbl 1412.68138) Full Text: DOI
Bliss, Donald B.; Epstein, Ronald J. Novel approach to aerodynamic analysis using analytical/numerical matching. (English) Zbl 0910.76054 AIAA J. 34, No. 11, 2225-2232 (1996). MSC: 76M25 76H05 PDF BibTeX XML Cite \textit{D. B. Bliss} and \textit{R. J. Epstein}, AIAA J. 34, No. 11, 2225--2232 (1996; Zbl 0910.76054) Full Text: DOI
Narendran, Paliath; Rusinowitch, Michaël Any ground associative-commutative theory has a finite canonical system. (English) Zbl 0878.68076 J. Autom. Reasoning 17, No. 1, 131-143 (1996). MSC: 68Q42 68T15 PDF BibTeX XML Cite \textit{P. Narendran} and \textit{M. Rusinowitch}, J. Autom. Reasoning 17, No. 1, 131--143 (1996; Zbl 0878.68076) Full Text: DOI
Jessee, J. P.; Fiveland, W. A. A cell vertex algorithm for the incompressible Navier-Stokes equations on non-orthogonal grids. (English) Zbl 0888.76068 Int. J. Numer. Methods Fluids 23, No. 3, 271-293 (1996). Reviewer: Th.Sonar (Hamburg) MSC: 76M25 76D05 PDF BibTeX XML Cite \textit{J. P. Jessee} and \textit{W. A. Fiveland}, Int. J. Numer. Methods Fluids 23, No. 3, 271--293 (1996; Zbl 0888.76068) Full Text: DOI
Linton, S.; Shand, D. Some group theoretic examples with completion theorem provers. (English) Zbl 0855.68087 J. Autom. Reasoning 17, No. 2, 145-169 (1996). MSC: 68T15 20-04 PDF BibTeX XML Cite \textit{S. Linton} and \textit{D. Shand}, J. Autom. Reasoning 17, No. 2, 145--169 (1996; Zbl 0855.68087) Full Text: DOI
Kapur, Deepak; Subramaniam, M. New uses of linear arithmetic in automated theorem proving by induction. (English) Zbl 0851.03002 J. Autom. Reasoning 16, No. 1-2, 39-78 (1996). Reviewer: D.Basin (Saarbrücken) MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{D. Kapur} and \textit{M. Subramaniam}, J. Autom. Reasoning 16, No. 1--2, 39--78 (1996; Zbl 0851.03002) 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 PDF BibTeX XML Cite \textit{C. Fermüller} and \textit{A. Leitsch}, J. Log. Comput. 6, No. 2, 173--203 (1996; Zbl 0861.68086) Full Text: DOI
Hähnle, Reiner Exploiting data dependencies in many-valued logics. (English) Zbl 0836.03013 J. Appl. Non-Class. Log. 6, No. 1, 49-69 (1996). MSC: 03B35 03B50 68T15 PDF BibTeX XML Cite \textit{R. Hähnle}, J. Appl. Non-Class. Log. 6, No. 1, 49--69 (1996; Zbl 0836.03013) Full Text: DOI
Niemelä, Ilkka A decision method for nonmonotonic reasoning based on autoepistemic reasoning. (English) Zbl 0826.03007 J. Autom. Reasoning 14, No. 1, 3-42 (1995). Reviewer: H.J.Ohlbach (Saarbrücken) MSC: 03B35 03B60 03B25 68Q25 PDF BibTeX XML Cite \textit{I. Niemelä}, J. Autom. Reasoning 14, No. 1, 3--42 (1995; Zbl 0826.03007) Full Text: DOI
Hähnle, Reiner Many-valued logic and mixed integer programming. (English) Zbl 0856.03011 Ann. Math. Artif. Intell. 12, No. 3-4, 231-263 (1994). MSC: 03B35 03B50 68T15 03B05 90C10 68Q25 03D15 PDF BibTeX XML Cite \textit{R. Hähnle}, Ann. Math. Artif. Intell. 12, No. 3--4, 231--263 (1994; Zbl 0856.03011) Full Text: DOI
Carrà Ferro, Giuseppa An extension of a procedure to prove statements in differential geometry. (English) Zbl 0808.03005 J. Autom. Reasoning 12, No. 3, 351-358 (1994). MSC: 03B35 68Q42 68T15 PDF BibTeX XML Cite \textit{G. Carrà Ferro}, J. Autom. Reasoning 12, No. 3, 351--358 (1994; Zbl 0808.03005) Full Text: DOI
Horn, Christian; Smaill, Alan From meta-level tactics to object-level programs. (English) Zbl 0801.03011 Johnson, Jeffrey (ed.) et al., Artificial intelligence in mathematics. Based on the proceedings of a conference, organized by The Institute of Mathematics and its Applications hosted by the University of Strathclyde, Glasgow, GB, and the Turing Institute in April 1991. Oxford: Clarendon Press. Inst. Math. Appl. Conf. Ser., New Ser. 51, 135-146 (1994). MSC: 03B35 68T15 68N15 03F35 PDF BibTeX XML Cite \textit{C. Horn} and \textit{A. Smaill}, in: Artificial intelligence in mathematics. Based on the proceedings of a conference, organized by The Institute of Mathematics and its Applications hosted by the University of Strathclyde, Glasgow, GB, and the Turing Institute in April 1991. Oxford: Clarendon Press. 135--146 (1994; Zbl 0801.03011)
Cantone, Domenico; Cutello, Vincenzo Decision procedures for stratified set-theoretic syllogistics. (Extended abstract). (English) Zbl 0921.03007 Bronstein, Manuel (ed.), ISSAC ’93. Proceedings of the 1993 international symposium on Symbolic and algebraic computation, Kiev, Ukraine, July 6–8, 1993. Baltimore, MD: ACM Press. 105-110 (1993). MSC: 03B25 03E30 03B35 68T15 03C13 PDF BibTeX XML Cite \textit{D. Cantone} and \textit{V. Cutello}, in: ISSAC '93. Proceedings of the 1993 international symposium on Symbolic and algebraic computation, Kiev, Ukraine, July 6--8, 1993. Baltimore, MD: ACM Press. 105--110 (1993; Zbl 0921.03007)
Manzari, M. T.; Lyra, P. R. M.; Morgan, K.; Peraire, J. An unstructured grid FEM/MUSCL algorithm for the compressible Euler equations. (English) Zbl 0874.76065 Morgan, K. (ed.) et al., Finite elements in fluids: new trends and applications. Proceedings of the 8th international conference, Barcelona, Spain, September 20-23, 1993. Part I. Barcelona: Centro Internacional de Métodos Numéricos en Ingeniería. 379-388 (1993). MSC: 76M25 76M10 76K05 PDF BibTeX XML Cite \textit{M. T. Manzari} et al., in: Finite elements in fluids: new trends and applications. Proceedings of the 8th international conference, Barcelona, Spain, September 20-23, 1993. Part I. Barcelona: Centro Internacional de Métodos Numéricos en Ingeniería; Swansea: Pineridge Press. 379--388 (1993; Zbl 0874.76065)
Bachmair, Leo; Ganzinger, Harald; Waldmann, Uwe Superposition with simplification as a decision procedure for the monadic class with equality. (English) Zbl 0793.68127 Gottlob, Georg (ed.) et al., Computational logic and proof theory. 3rd Kurt Gödel Colloquium, KGC ’93, Brno, Czech Republic, August 24-27, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 713, 83-96 (1993). MSC: 68T15 03B25 PDF BibTeX XML Cite \textit{L. Bachmair} et al., Lect. Notes Comput. Sci. 713, 83--96 (1993; Zbl 0793.68127)
Nadathur, Gopalan A proof procedure for the logic of hereditary Harrop formulas. (English) Zbl 0796.03012 J. Autom. Reasoning 11, No. 1, 115-145 (1993). Reviewer: N.Zamov (Kazan’) MSC: 03B35 03B20 68N17 68T15 PDF BibTeX XML Cite \textit{G. Nadathur}, J. Autom. Reasoning 11, No. 1, 115--145 (1993; Zbl 0796.03012) Full Text: DOI
Snyder, Wayne On the complexity of recursive path orderings. (English) Zbl 0778.68045 Inf. Process. Lett. 46, No. 5, 257-262 (1993). Reviewer: Wayne Snyder MSC: 68Q25 68T15 68Q42 PDF BibTeX XML Cite \textit{W. Snyder}, Inf. Process. Lett. 46, No. 5, 257--262 (1993; Zbl 0778.68045) Full Text: DOI
Gallier, Jean; Narendran, Paliath; Plaisted, David; Raatz, Stan; Snyder, Wayne An algorithm for finding canonical sets of ground rewrite rules in polynomial time. (English) Zbl 0779.68050 J. Assoc. Comput. Mach. 40, No. 1, 1-16 (1993). Reviewer: D.Lucanu (Iaşi) MSC: 68Q42 68Q25 68T15 PDF BibTeX XML Cite \textit{J. Gallier} et al., J. Assoc. Comput. Mach. 40, No. 1, 1--16 (1993; Zbl 0779.68050) Full Text: DOI
Tu, Xin M.; Burdick, Donald S. Resolution of trilinear mixtures: Application in spectroscopy. (English) Zbl 0828.62103 Stat. Sin. 2, No. 2, 577-593 (1992). MSC: 62P99 62H25 PDF BibTeX XML Cite \textit{X. M. Tu} and \textit{D. S. Burdick}, Stat. Sin. 2, No. 2, 577--593 (1992; Zbl 0828.62103)
Lee, Shie-Jue; Plaisted, David A. Eliminating dublication with the hyper-linking strategy. (English) Zbl 0784.68077 J. Autom. Reasoning 9, No. 1, 25-42 (1992). MSC: 68T15 PDF BibTeX XML Cite \textit{S.-J. Lee} and \textit{D. A. Plaisted}, J. Autom. Reasoning 9, No. 1, 25--42 (1992; Zbl 0784.68077) Full Text: DOI