Aït-Kaci, Hassan; Pasi, Gabriella Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach. (English) Zbl 1452.06008 Fuzzy Sets Syst. 391, 1-46 (2020). MSC: 06D72 68N17 PDF BibTeX XML Cite \textit{H. Aït-Kaci} and \textit{G. Pasi}, Fuzzy Sets Syst. 391, 1--46 (2020; Zbl 1452.06008) Full Text: DOI
Calimeri, Francesco; Ianni, Giovambattista; Pacenza, Francesco; Perri, Simona; Zangari, Jessica Incremental answer set programming with overgrounding. (English) Zbl 1434.68555 Theory Pract. Log. Program. 19, No. 5-6, 957-973 (2019). MSC: 68T27 68N17 68T30 PDF BibTeX XML Cite \textit{F. Calimeri} et al., Theory Pract. Log. Program. 19, No. 5--6, 957--973 (2019; Zbl 1434.68555) Full Text: DOI
Leitsch, Alexander; Lolic, Anela Extraction of expansion trees. (English) Zbl 07038742 J. Autom. Reasoning 62, No. 3, 393-430 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{A. Leitsch} and \textit{A. Lolic}, J. Autom. Reasoning 62, No. 3, 393--430 (2019; Zbl 07038742) Full Text: DOI
Goldberg, Paul W.; Papadimitriou, Christos H. Towards a unified complexity theory of total functions. (English) Zbl 1393.68053 J. Comput. Syst. Sci. 94, 167-192 (2018). Reviewer: Gregory Loren McColm (Tampa) MSC: 68Q15 03F20 68Q17 68Q25 PDF BibTeX XML Cite \textit{P. W. Goldberg} and \textit{C. H. Papadimitriou}, J. Comput. Syst. Sci. 94, 167--192 (2018; Zbl 1393.68053) Full Text: DOI
Eberhard, Sebastian; Hetzl, Stefan On the compressibility of finite languages and formal proofs. (English) Zbl 1390.68389 Inf. Comput. 259, Part 2, 191-213 (2018). MSC: 68Q45 03F20 68Q42 PDF BibTeX XML Cite \textit{S. Eberhard} and \textit{S. Hetzl}, Inf. Comput. 259, Part 2, 191--213 (2018; Zbl 1390.68389) Full Text: DOI
Eberhard, Sebastian; Hetzl, Stefan Inductive theorem proving based on tree grammars. (English) Zbl 1386.03018 Ann. Pure Appl. Logic 166, No. 6, 665-700 (2015). MSC: 03B35 03F07 03F03 03F30 68Q42 68T15 PDF BibTeX XML Cite \textit{S. Eberhard} and \textit{S. Hetzl}, Ann. Pure Appl. Logic 166, No. 6, 665--700 (2015; Zbl 1386.03018) Full Text: DOI
Hazen, Allen P.; Pelletier, Francis Jeffry Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different. (English) Zbl 1344.03044 Stud. Log. 102, No. 6, 1103-1142 (2014). MSC: 03F03 03F07 03-03 01A60 03B05 03B20 PDF BibTeX XML Cite \textit{A. P. Hazen} and \textit{F. J. Pelletier}, Stud. Log. 102, No. 6, 1103--1142 (2014; Zbl 1344.03044) Full Text: DOI
Paleo, Bruno Woltzenlogel Physics and proof theory. (English) Zbl 1291.81015 Appl. Math. Comput. 219, No. 1, 45-53 (2012). MSC: 81P05 03F07 PDF BibTeX XML Cite \textit{B. W. Paleo}, Appl. Math. Comput. 219, No. 1, 45--53 (2012; Zbl 1291.81015) Full Text: DOI
Hakli, Raul; Negri, Sara Does the deduction theorem fail for modal logic? (English) Zbl 1275.03091 Synthese 187, No. 3, 849-867 (2012). MSC: 03B45 PDF BibTeX XML Cite \textit{R. Hakli} and \textit{S. Negri}, Synthese 187, No. 3, 849--867 (2012; Zbl 1275.03091) Full Text: DOI
Chvalovský, Karel; Cintula, Petr Note on deduction theorems in contraction-free logics. (English) Zbl 1248.03014 Math. Log. Q. 58, No. 3, 236-243 (2012). MSC: 03B22 03B47 PDF BibTeX XML Cite \textit{K. Chvalovský} and \textit{P. Cintula}, Math. Log. Q. 58, No. 3, 236--243 (2012; Zbl 1248.03014) Full Text: DOI
Areces, Carlos; Gorín, Daniel Resolution with order and selection for hybrid logics. (English) Zbl 1227.03016 J. Autom. Reasoning 46, No. 1, 1-42 (2011). Reviewer: Nail Zamov (Kazan) MSC: 03B35 03B45 PDF BibTeX XML Cite \textit{C. Areces} and \textit{D. Gorín}, J. Autom. Reasoning 46, No. 1, 1--42 (2011; Zbl 1227.03016) Full Text: DOI
Willard, Dan E. Some specially formulated axiomizations for \(\mathrm{I}\Sigma _0\) manage to evade the Herbrandized version of the second incompleteness theorem. (English) Zbl 1191.03044 Inf. Comput. 207, No. 10, 1078-1093 (2009). Reviewer: Saeed Salehi (Tabriz) MSC: 03F40 PDF BibTeX XML Cite \textit{D. E. Willard}, Inf. Comput. 207, No. 10, 1078--1093 (2009; Zbl 1191.03044) Full Text: DOI
Craig, William The road to two theorems of logic. (English) Zbl 1171.03017 Synthese 164, No. 3, 333-339 (2008). MSC: 03C40 03-03 01A60 PDF BibTeX XML Cite \textit{W. Craig}, Synthese 164, No. 3, 333--339 (2008; Zbl 1171.03017) Full Text: DOI
Willard, Dan E. The axiom system \(\mathrm{I}\Sigma_{0}\) manages to simultaneously obey and evade the Herbrandized version of the second incompleteness theorem. (English) Zbl 1262.03122 Mints, G. (ed.) et al., Proceedings of the 13th workshop on logic, language, information and computation (WoLLIC 2006), Stanford, CA, USA, July 18–21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 165, 213-226 (2006). MSC: 03F30 03F40 PDF BibTeX XML Cite \textit{D. E. Willard}, Electron. Notes Theor. Comput. Sci. 165, 213--226 (2006; Zbl 1262.03122) Full Text: DOI
Hughes, Dominic J. D. Towards Hilbert’s 24th problem: combinatorial proof invariants (preliminary version). (English) Zbl 1262.03120 Mints, G. (ed.) et al., Proceedings of the 13th workshop on logic, language, information and computation (WoLLIC 2006), Stanford, CA, USA, July 18–21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 165, 37-63 (2006). MSC: 03F07 03F05 PDF BibTeX XML Cite \textit{D. J. D. Hughes}, Electron. Notes Theor. Comput. Sci. 165, 37--63 (2006; Zbl 1262.03120) Full Text: DOI
Baaz, Matthias; Iemhoff, Rosalie The Skolemization of existential quantifiers in intuitionistic logic. (English) Zbl 1106.03004 Ann. Pure Appl. Logic 142, No. 1-3, 269-295 (2006). Reviewer: Osamu Sonobe (Follonica) MSC: 03B20 03B25 PDF BibTeX XML Cite \textit{M. Baaz} and \textit{R. Iemhoff}, Ann. Pure Appl. Logic 142, No. 1--3, 269--295 (2006; Zbl 1106.03004) Full Text: DOI
Duda, Roman On the Warsaw interactions of logic and mathematics in the years 1919–1939. (English) Zbl 1058.03003 Ann. Pure Appl. Logic 127, No. 1-3, 289-301 (2004). Reviewer: Teun Koetsier (Amsterdam) MSC: 03-03 01A60 01A72 03E10 03E25 03E50 PDF BibTeX XML Cite \textit{R. Duda}, Ann. Pure Appl. Logic 127, No. 1--3, 289--301 (2004; Zbl 1058.03003) Full Text: DOI
Goguen, Joseph; Malcolm, Grant; Kemp, Tom A hidden Herbrand theorem: Combining the object and logic paradigms. (English) Zbl 1012.03041 J. Log. Algebr. Program. 51, No. 1, 1-41 (2002). MSC: 03B70 68N30 PDF BibTeX XML Cite \textit{J. Goguen} et al., J. Log. Algebr. Program. 51, No. 1, 1--41 (2002; Zbl 1012.03041) Full Text: DOI
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude Higher order unification via explicit substitutions. (English) Zbl 1005.03016 Inf. Comput. 157, No. 1-2, 183-235 (2000). MSC: 03B40 03B15 03B35 68Q42 PDF BibTeX XML Cite \textit{G. Dowek} et al., Inf. Comput. 157, No. 1--2, 183--235 (2000; Zbl 1005.03016) Full Text: DOI
Buss, Samuel R. Bounded arithmetic, proof complexity and two papers of Parikh. (English) Zbl 0924.03106 Ann. Pure Appl. Logic 96, No. 1-3, 43-55 (1999). Reviewer: M.Tetruašvili (Tbilisi) MSC: 03F30 03F20 03F07 68Q15 PDF BibTeX XML Cite \textit{S. R. Buss}, Ann. Pure Appl. Logic 96, No. 1--3, 43--55 (1999; Zbl 0924.03106) Full Text: DOI
Fokkink, Wan Unification for infinite sets of equations between finite terms. (English) Zbl 1337.68238 Inf. Process. Lett. 62, No. 4, 183-188 (1997). MSC: 68T15 PDF BibTeX XML Cite \textit{W. Fokkink}, Inf. Process. Lett. 62, No. 4, 183--188 (1997; Zbl 1337.68238) Full Text: DOI
Weibel, Trudy An order-sorted resolution in theory and practice. (English) Zbl 0901.68041 Theor. Comput. Sci. 185, No. 2, 393-410 (1997). MSC: 68P10 PDF BibTeX XML Cite \textit{T. Weibel}, Theor. Comput. Sci. 185, No. 2, 393--410 (1997; Zbl 0901.68041) Full Text: DOI
Bürckert, Hans-Jürgen; Hollunder, Bernhard; Laux, Armin On Skolemization in constrained logics. (English) Zbl 0887.03005 Ann. Math. Artif. Intell. 18, No. 2-4, 95-131 (1996). MSC: 03B35 03B10 PDF BibTeX XML Cite \textit{H.-J. Bürckert} et al., Ann. Math. Artif. Intell. 18, No. 2--4, 95--131 (1996; Zbl 0887.03005) Full Text: DOI
Albert, Luc; Casas, Rafael; Fages, François Average-case analysis of unification algorithms. (English) Zbl 0779.68043 Theor. Comput. Sci. 113, No. 1, 3-34 (1993). Reviewer: L.Albert MSC: 68Q25 68N17 68W30 PDF BibTeX XML Cite \textit{L. Albert} et al., Theor. Comput. Sci. 113, No. 1, 3--34 (1993; Zbl 0779.68043) Full Text: DOI
Dougherty, Daniel J.; Johann, Patricia An improved general \(E\)-unification method. (English) Zbl 0773.68063 J. Symb. Comput. 14, No. 4, 303-320 (1992). MSC: 68T15 PDF BibTeX XML Cite \textit{D. J. Dougherty} and \textit{P. Johann}, J. Symb. Comput. 14, No. 4, 303--320 (1992; Zbl 0773.68063) Full Text: DOI
Beierle, C.; Hedtstück, U.; Pletat, U.; Schmitt, P. H.; Siekmann, J. An order-sorted logic for knowledge representation systems. (English) Zbl 0768.68196 Artif. Intell. 55, No. 2-3, 149-191 (1992). MSC: 68T27 68T30 PDF BibTeX XML Cite \textit{C. Beierle} et al., Artif. Intell. 55, No. 2--3, 149--191 (1992; Zbl 0768.68196) Full Text: DOI
Baaz, Matthias; Leitsch, Alexander Complexity of resolution proofs and function introduction. (English) Zbl 0769.03009 Ann. Pure Appl. Logic 57, No. 3, 181-215 (1992). Reviewer: G.Mints (Stanford) MSC: 03B35 03F20 PDF BibTeX XML Cite \textit{M. Baaz} and \textit{A. Leitsch}, Ann. Pure Appl. Logic 57, No. 3, 181--215 (1992; Zbl 0769.03009) Full Text: DOI
Burris, Stanley Discriminator varieties and symbolic computation. (English) Zbl 0803.08002 J. Symb. Comput. 13, No. 2, 175-207 (1992). MSC: 08B05 08A70 68W30 PDF BibTeX XML Cite \textit{S. Burris}, J. Symb. Comput. 13, No. 2, 175--207 (1992; Zbl 0803.08002) Full Text: DOI
Farmer, William M. Simple second-order languages for which unification is undecidable. (English) Zbl 0731.03005 Theor. Comput. Sci. 87, No. 1, 25-41 (1991). Reviewer: G.Mints (Stanford) MSC: 03B15 68T15 03B25 03B35 PDF BibTeX XML Cite \textit{W. M. Farmer}, Theor. Comput. Sci. 87, No. 1, 25--41 (1991; Zbl 0731.03005) Full Text: DOI
Bacchus, Fahiem; Tenenberg, Josh; Koomen, Johannes A. A non-reified temporal logic. (English) Zbl 0762.03009 Artif. Intell. 52, No. 1, 87-108 (1991). Reviewer: G.Saake (Braunschweig) MSC: 03B45 68T27 68T30 PDF BibTeX XML Cite \textit{F. Bacchus} et al., Artif. Intell. 52, No. 1, 87--108 (1991; Zbl 0762.03009) Full Text: DOI
Doggaz, Narjes; Kirchner, Claude Completion for unification. (English) Zbl 0735.68078 Theor. Comput. Sci. 85, No. 2, 231-251 (1991). Reviewer: M.Armbrust MSC: 68T99 68T15 68N17 PDF BibTeX XML Cite \textit{N. Doggaz} and \textit{C. Kirchner}, Theor. Comput. Sci. 85, No. 2, 231--251 (1991; Zbl 0735.68078) Full Text: DOI
Gallier, Jean; Narendran, Paliath; Plaisted, David; Snyder, Wayne Rigid E-unification: NP-completeness and applications to equational matings. (English) Zbl 0709.68080 Inf. Comput. 87, No. 1-2, 129-195 (1990). Reviewer: M.Armbrust MSC: 68T15 68Q25 03B35 PDF BibTeX XML Cite \textit{J. Gallier} et al., Inf. Comput. 87, No. 1--2, 129--195 (1990; Zbl 0709.68080) Full Text: DOI
Schmidt-Schauß, Manfred Unification in a combination of arbitrary disjoint equational theories. (English) Zbl 0691.03003 J. Symb. Comput. 8, No. 1-2, 51-99 (1989). Reviewer: C.Masalagiu MSC: 03B35 03C05 08B05 PDF BibTeX XML Cite \textit{M. Schmidt-Schauß}, J. Symb. Comput. 8, No. 1--2, 51--99 (1989; Zbl 0691.03003) Full Text: DOI
Meseguer, José; Goguen, Joseph A.; Smolka, Gert Order-sorted unification. (English) Zbl 0691.03002 J. Symb. Comput. 8, No. 4, 383-413 (1989). Reviewer: C.Masalagiu MSC: 03B35 08B05 PDF BibTeX XML Cite \textit{J. Meseguer} et al., J. Symb. Comput. 8, No. 4, 383--413 (1989; Zbl 0691.03002) Full Text: DOI
Boudet, Alexandre; Jouannaud, Jean-Pierre; Schmidt-Schauss, Manfred Unification in Boolean rings and Abelian groups. (English) Zbl 0689.68040 J. Symb. Comput. 8, No. 5, 449-477 (1989). MSC: 68W30 06E20 68Q65 PDF BibTeX XML Cite \textit{A. Boudet} et al., J. Symb. Comput. 8, No. 5, 449--477 (1989; Zbl 0689.68040) Full Text: DOI
Casas, R.; Diaz, J.; Steyaert, J. M. Average-case analysis of Robinson’s unification algorithm with two different variables. (English) Zbl 0681.68058 Inf. Process. Lett. 31, No. 5, 227-232 (1989). MSC: 68Q25 68W30 68T15 68T99 PDF BibTeX XML Cite \textit{R. Casas} et al., Inf. Process. Lett. 31, No. 5, 227--232 (1989; Zbl 0681.68058) Full Text: DOI
Smolka, Gert; Ait-Kaci, Hassan Inheritance hierarchies: Semantics and unifications. (English) Zbl 0678.68009 J. Symb. Comput. 7, No. 3-4, 343-370 (1989). MSC: 68Q60 68T15 68W30 68Q65 PDF BibTeX XML Cite \textit{G. Smolka} and \textit{H. Ait-Kaci}, J. Symb. Comput. 7, No. 3--4, 343--370 (1989; Zbl 0678.68009) Full Text: DOI
Buchberger, Bruno History and basic features of the critical-pair/completion procedure. (English) Zbl 0645.68094 J. Symb. Comput. 3, 3-38 (1987). MSC: 68T15 68W30 68Q45 08A50 01-02 68-03 PDF BibTeX XML Cite \textit{B. Buchberger}, J. Symb. Comput. 3, 3--38 (1987; Zbl 0645.68094) Full Text: DOI
Coquand, Thierry; Huet, Gérard A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction. (English) Zbl 0591.68036 J. Symb. Comput. 1, 323-328 (1985). MSC: 68Q65 68Q60 03Fxx 03B35 03B15 03B40 03F55 68T15 00A15 PDF BibTeX XML Cite \textit{T. Coquand} and \textit{G. Huet}, J. Symb. Comput. 1, 323--328 (1985; Zbl 0591.68036) Full Text: DOI
Walther, Christoph A mechanical solution of Schubert’s steamroller by many-sorted resolution. (English) Zbl 0569.68076 Artif. Intell. 26, 217-224 (1985). MSC: 68T15 PDF BibTeX XML Cite \textit{C. Walther}, Artif. Intell. 26, 217--224 (1985; Zbl 0569.68076) Full Text: DOI
Nossum, Rolf Automated theorem proving methods. (English) Zbl 0564.03016 BIT 25, 51-64 (1985). Reviewer: H.P.Schmitt MSC: 03B35 68T15 PDF BibTeX XML Cite \textit{R. Nossum}, BIT 25, 51--64 (1985; Zbl 0564.03016) Full Text: DOI
Joseph, Deborah Polynomial time computations in models of ET. (English) Zbl 0542.03019 J. Comput. Syst. Sci. 26, 311-338 (1983). Reviewer: R.Murawski MSC: 03D15 03H15 PDF BibTeX XML Cite \textit{D. Joseph}, J. Comput. Syst. Sci. 26, 311--338 (1983; Zbl 0542.03019) Full Text: DOI
Wirsing, Martin Kleine unentscheidbare Klassen der Prädikatenlogik mit Identität und Funktionszeichen. (German) Zbl 0398.03005 Arch. Math. Logik Grundlagenforsch. 19, 97-109 (1978). MSC: 03B10 03B25 PDF BibTeX XML Cite \textit{M. Wirsing}, Arch. Math. Logik Grundlagenforsch. 19, 97--109 (1978; Zbl 0398.03005) Full Text: DOI EuDML
Orlowska, Ewa On the Jaskowski’s method of suppositions. (English) Zbl 0325.02022 Stud. Log. 34, 187-200 (1975). MSC: 03F99 03-03 01A60 PDF BibTeX XML Cite \textit{E. Orlowska}, Stud. Log. 34, 187--200 (1975; Zbl 0325.02022) Full Text: DOI
Surma, Stanislaw J. Indirect-deduction theorems. (Polish) Zbl 0307.02021 Stud. Log. 20, 151-166 (1967). MSC: 03F99 03B05 PDF BibTeX XML Cite \textit{S. J. Surma}, Stud. Log. 20, 151--166 (1967; Zbl 0307.02021) Full Text: DOI
Iseki, K. On axiom systems of propositional calculi. IV. (English) Zbl 0156.24804 Proc. Japan Acad. 41, 575-577 (1965). PDF BibTeX XML Cite \textit{K. Iseki}, Proc. Japan Acad. 41, 575--577 (1965; Zbl 0156.24804) Full Text: DOI
Dreben, Burton; Andrews, Peter; Aanderaa, Stål O. False lemmas in Herbrand. (English) Zbl 0126.01006 Bull. Am. Math. Soc. 69, 699-706 (1963). PDF BibTeX XML Cite \textit{B. Dreben} et al., Bull. Am. Math. Soc. 69, 699--706 (1963; Zbl 0126.01006) Full Text: DOI
Oglesby, F. C. An examination of a decision procedure. (English) Zbl 0100.01004 Bull. Am. Math. Soc. 67, 300-304 (1961). PDF BibTeX XML Cite \textit{F. C. Oglesby}, Bull. Am. Math. Soc. 67, 300--304 (1961; Zbl 0100.01004) Full Text: DOI
Lightstone, A. H.; Robinson, A. Syntactical transfroms. (English) Zbl 0208.01001 Trans. Am. Math. Soc. 86, 220-245 (1957). MSC: 03B10 03B80 PDF BibTeX XML Cite \textit{A. H. Lightstone} and \textit{A. Robinson}, Trans. Am. Math. Soc. 86, 220--245 (1957; Zbl 0208.01001) Full Text: DOI
Schmidt, Arnold Über deduktive Theorien mit mehreren Sorten von Grunddingen. (German) Zbl 0018.33804 Math. Ann. 115, 485-506 (1938). PDF BibTeX XML Cite \textit{A. Schmidt}, Math. Ann. 115, 485--506 (1938; Zbl 0018.33804) Full Text: DOI EuDML
Schmidt, A. Über deduktive Theorien mit mehreren Sorten von Grunddingen. (German) JFM 64.0028.01 Math. Ann. 115, 485-506 (1938). Reviewer: Ackermann, W., Dr. (Burgsteinfurt) PDF BibTeX XML Cite \textit{A. Schmidt}, Math. Ann. 115, 485--506 (1938; JFM 64.0028.01) Full Text: DOI Link EuDML