Switch to: References

Citations of:

On Theories with a Combinatorial Definition of "Equivalence."

M. H. A. Newman

Journal of Symbolic Logic 7 (3):123-123 (1942)

Add citations

You must login to add citations.

Importing Logics.João Rasga, Amílcar Sernadas & Cristina Sernadas - 2012 - Studia Logica 100 (3):545-581.details The novel notion of importing logics is introduced, subsuming as special cases several kinds of asymmetric combination mechanisms, like temporalization [8, 9], modalization [7] and exogenous enrichment [13, 5, 12, 4, 1]. The graph-theoretic approach proposed in [15] is used, but formulas are identified with irreducible paths in the signature multi-graph instead of equivalence classes of such paths, facilitating proofs involving inductions on formulas. Importing is proved to be strongly conservative. Conservative results follow as corollaries for temporalization, modalization and exogenous (...) enrichment. (shrink) Download Export citation Bookmark 3 citations
Mω considered as a programming language.Karl-Heinz Niggl - 1999 - Annals of Pure and Applied Logic 99 (1-3):73-92.details The paper studies a simply typed term system Mω providing a primitive recursive concept of parallelism in the sense of Plotkin. The system aims at defining and computing partial continuous functionals. Some connections between denotational and operational semantics → for Mω are investigated. It is shown that → is correct with respect to the denotational semantics. Conversely, → is complete in the sense that if a program denotes some number k, then it is reducible to the numeral nk. Restricting to (...) Download Export citation Bookmark 1 citation
Refined program extraction from classical proofs.Ulrich Berger, Wilfried Buchholz & Helmut Schwichtenberg - 2002 - Annals of Pure and Applied Logic 114 (1-3):3-25.details The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula. Download Export citation Bookmark 9 citations
Logical Foundations for Hybrid Type-Logical Grammars.Richard Moot & Symon Jory Stevens-Guille - 2022 - Journal of Logic, Language and Information 31 (1):35-76.details This paper explores proof-theoretic aspects of hybrid type-logical grammars, a logic combining Lambek grammars with lambda grammars. We prove some basic properties of the calculus, such as normalisation and the subformula property and also present both a sequent and a proof net calculus for hybrid type-logical grammars. In addition to clarifying the logical foundations of hybrid type-logical grammars, the current study opens the way to variants and extensions of the original system, including but not limited to a non-associative version and (...) Download Export citation Bookmark
On Mathematicians Who Liked Logic.Ivor Grattan-Guinness - 2012 - In S. Barry Cooper (ed.), How the World Computes. pp. 245--252.details Download Export citation Bookmark
Modular termination of basic narrowing and equational unification.María Alpuente, Santiago Escobar & José Iborra - 2011 - Logic Journal of the IGPL 19 (6):731-762.details Basic narrowing is a restricted form of narrowing which constrains narrowing steps to a set of unblocked positions. In this work, we study the modularity of termination of basic narrowing in hierarchical combinations of TRSs, which provides new algorithmic criteria to prove termination of basic narrowing. Basic narrowing has a number of important applications including equational unification in canonical theories. Another application is analyzing termination of narrowing by checking the termination of basic narrowing, as done in pioneering work by Hullot. (...) Download Export citation Bookmark

1