Journal articles: 'Higher order logics'

1

Finkelstein, David. "Higher-order quantum logics." International Journal of Theoretical Physics 31, no. 9 (September 1992): 1627–38. http://dx.doi.org/10.1007/bf00671777.

Full text

APA, Harvard, Vancouver, ISO, and other styles

2

Hella, Lauri, and José M. Turull-Torres. "Expressibility of Higher Order Logics." Electronic Notes in Theoretical Computer Science 84 (September 2003): 129–40. http://dx.doi.org/10.1016/s1571-0661(04)80850-8.

Full text

APA, Harvard, Vancouver, ISO, and other styles

3

Aguirre, Alejandro, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, and Tetsuya Sato. "Higher-order probabilistic adversarial computations: categorical semantics and program logics." Proceedings of the ACM on Programming Languages 5, ICFP (August 22, 2021): 1–30. http://dx.doi.org/10.1145/3473598.

Full text

Abstract:

Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning. In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed λ-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples.

APA, Harvard, Vancouver, ISO, and other styles

4

Dal Lago, Ugo, Simone Martini, and Davide Sangiorgi. "Light Logics and Higher-Order Processes." Electronic Proceedings in Theoretical Computer Science 41 (November 28, 2010): 46–60. http://dx.doi.org/10.4204/eptcs.41.4.

Full text

APA, Harvard, Vancouver, ISO, and other styles

5

DAL LAGO, UGO, SIMONE MARTINI, and DAVIDE SANGIORGI. "Light logics and higher-order processes." Mathematical Structures in Computer Science 26, no. 6 (November 17, 2014): 969–92. http://dx.doi.org/10.1017/s0960129514000310.

Full text

Abstract:

We show that the techniques for resource control that have been developed by the so-calledlight logicscan be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

APA, Harvard, Vancouver, ISO, and other styles

6

Hella, Lauri, and José María Turull-Torres. "Computing queries with higher-order logics." Theoretical Computer Science 355, no. 2 (April 2006): 197–214. http://dx.doi.org/10.1016/j.tcs.2006.01.009.

Full text

APA, Harvard, Vancouver, ISO, and other styles

7

Crary, Karl. "Higher-order representation of substructural logics." ACM SIGPLAN Notices 45, no. 9 (September 27, 2010): 131–42. http://dx.doi.org/10.1145/1932681.1863565.

Full text

APA, Harvard, Vancouver, ISO, and other styles

8

Benzmüller, Christoph, Dov Gabbay, Valerio Genovese, and Daniele Rispoli. "Embedding and automating conditional logics in classical higher-order logic." Annals of Mathematics and Artificial Intelligence 66, no. 1-4 (September 25, 2012): 257–71. http://dx.doi.org/10.1007/s10472-012-9320-z.

Full text

APA, Harvard, Vancouver, ISO, and other styles

9

Andrews, James H. "An untyped higher order logic with Y combinator." Journal of Symbolic Logic 72, no. 4 (December 2007): 1385–404. http://dx.doi.org/10.2178/jsl/1203350794.

Full text

Abstract:

AbstractWe define a higher order logic which has only a notion of sort rather than a notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory, a proof system which is sound with respect to the model theory, and a cut-elimination proof for the proof system. We also give examples showing what formulas can and cannot be used in the logic.

APA, Harvard, Vancouver, ISO, and other styles

10

Sági, Gábor. "A completeness theorem for higher order logics." Journal of Symbolic Logic 65, no. 2 (June 2000): 857–84. http://dx.doi.org/10.2307/2586575.

Full text

Abstract:

AbstractHere we investigate the classes of representable directed cylindric algebras of dimension α introduced by Németi [12]. can be seen in two different ways: first, as an algebraic counterpart of higher order logics and second, as a cylindric algebraic analogue of Quasi-Projective Relation Algebras. We will give a new, “purely cylindric algebraic” proof for the following theorems of Németi: (i) is a finitely axiomatizable variety whenever α ≥ 3 is finite and (ii) one can obtain a strong representation theorem for if one chooses an appropriate (non-well-founded) set theory as foundation of mathematics. These results provide a purely cylindric algebraic solution for the Finitization Problem (in the sense of [11]) in some non-well-founded set theories.

APA, Harvard, Vancouver, ISO, and other styles

11

Steen, Alexander. "Higher-order theorem proving and its applications." it - Information Technology 61, no. 4 (August 27, 2019): 187–91. http://dx.doi.org/10.1515/itit-2019-0001.

Full text

Abstract:

Abstract Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed.

APA, Harvard, Vancouver, ISO, and other styles

12

Benzmüller, Christoph. "Combining and automating classical and non-classical logics in classical higher-order logics." Annals of Mathematics and Artificial Intelligence 62, no. 1-2 (June 2011): 103–28. http://dx.doi.org/10.1007/s10472-011-9249-7.

Full text

APA, Harvard, Vancouver, ISO, and other styles

13

Mamdani, E. H., and H. J. Efstathiou. "Higher-order logics for handling uncertainty in expert systems." International Journal of Man-Machine Studies 22, no. 3 (March 1985): 283–93. http://dx.doi.org/10.1016/s0020-7373(85)80004-3.

Full text

APA, Harvard, Vancouver, ISO, and other styles

14

UMEZAWA, Toshio. "An extension of intermediate predicate logics to higher order." Japanese journal of mathematics. New series 17, no. 1 (1991): 37–55. http://dx.doi.org/10.4099/math1924.17.37.

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

Ferrarotti, Flavio Antonio, and José María Turull Torres. "Arity and alternation: a proper hierarchy in higher order logics." Annals of Mathematics and Artificial Intelligence 50, no. 1-2 (July 18, 2007): 111–41. http://dx.doi.org/10.1007/s10472-007-9071-4.

Full text

APA, Harvard, Vancouver, ISO, and other styles

16

Zaionc, Marek. "On the λ Definable Higher Order Boolean Operations." Fundamenta Informaticae 12, no. 2 (April 1, 1989): 181–89. http://dx.doi.org/10.3233/fi-1989-12205.

Full text

Abstract:

The purpose of this work is to show the methods of representing higher order boolean functionals in the simple typed λ calculus. In the paper is presented an algorithm for construction the λ representation of a functional given by generalized truth table. This technique is useful especially in functional programming languages such as ML in which functionals are expressed in the form of typed λ terms. Also λ representability of higher order functionals in many valued logics is discussed.

APA, Harvard, Vancouver, ISO, and other styles

17

Doder, Dragan, Nenad Savić, and Zoran Ognjanović. "Multi-agent Logics for Reasoning About Higher-Order Upper and Lower Probabilities." Journal of Logic, Language and Information 29, no. 1 (September 3, 2019): 77–107. http://dx.doi.org/10.1007/s10849-019-09301-7.

Full text

APA, Harvard, Vancouver, ISO, and other styles

18

Găină, Daniel, and Tomasz Kowalski. "Fraïssé–Hintikka theorem in institutions." Journal of Logic and Computation 30, no. 7 (September 3, 2020): 1377–99. http://dx.doi.org/10.1093/logcom/exaa042.

Full text

Abstract:

Abstract We generalize the characterization of elementary equivalence by Ehrenfeucht–Fraïssé games to arbitrary institutions whose sentences are finitary. These include many-sorted first-order logic, higher-order logic with types, as well as a number of other logics arising in connection to specification languages. The gain for the classical case is that the characterization is proved directly for all signatures, including infinite ones.

APA, Harvard, Vancouver, ISO, and other styles

19

Despeyroux, Joëlle, and Robert Harper. "Special issue on Logical Frameworks and Metalanguages http//www-sop.inria.fr/certilab/LFM00/cfp-jfp.html." Journal of Functional Programming 10, no. 1 (January 2000): 135–36. http://dx.doi.org/10.1017/s0956796899009892.

Full text

Abstract:

Logical frameworks and meta-languages are intended as a common substrate for representing and implementing a wide variety of logics and formal systems. Their definition and implementation have been the focus of considerable work over the last decade. At the heart of this work is a quest for generality: A logical framework provides a basis for capturing uniformities across deductive systems and support for implementing particular systems. Similarly a meta-language supports reasoning about and using languages.Logical frameworks have been based on a variety of different languages including higher-order logics, type theories with dependent types, linear logic, and modal logic. Techniques of representation of logics include higher-order abstract syntax, inductive definitions or some form of equational or rewriting logic in which substitution is explicitly encoded.Examples of systems that implement logical frameworks include Alf, Coq, NuPrl, HOL, Isabelle, Maude, lambda-Prolog and Twelf. An active area of research in such systems is the study of automated reasoning techniques. Current work includes the development of various automated procedures as well as the investigation of rewriting tools that use reflection or make use of links with systems that already have sophisticated rewriting systems. Program extraction and optimization are additional topics of ongoing work.

APA, Harvard, Vancouver, ISO, and other styles

20

HUET, GÉRARD. "Special issue on ‘Logical frameworks and metalanguages’." Journal of Functional Programming 13, no. 2 (March 2003): 257–60. http://dx.doi.org/10.1017/s0956796802004549.

Full text

Abstract:

There is both a great unity and a great diversity in presentations of logic. The diversity is staggering indeed – propositional logic, first-order logic, higher-order logic belong to one classification; linear logic, intuitionistic logic, classical logic, modal and temporal logics belong to another one. Logical deduction may be presented as a Hilbert style of combinators, as a natural deduction system, as sequent calculus, as proof nets of one variety or other, etc. Logic, originally a field of philosophy, turned into algebra with Boole, and more generally into meta-mathematics with Frege and Heyting. Professional logicians such as Gödel and later Tarski studied mathematical models, consistency and completeness, computability and complexity issues, set theory and foundations, etc. Logic became a very technical area of mathematical research in the last half century, with fine-grained analysis of expressiveness of subtheories of arithmetic or set theory, detailed analysis of well-foundedness through ordinal notations, logical complexity, etc. Meanwhile, computer modelling developed a need for concrete uses of logic, first for the design of computer circuits, then more widely for increasing the reliability of sofware through the use of formal specifications and proofs of correctness of computer programs. This gave rise to more exotic logics, such as dynamic logic, Hoare-style logic of axiomatic semantics, logics of partial values (such as Scott's denotational semantics and Plotkin's domain theory) or of partial terms (such as Feferman's free logic), etc. The first actual attempts at mechanisation of logical reasoning through the resolution principle (automated theorem proving) had been disappointing, but their shortcomings gave rise to a considerable body of research, developing detailed knowledge about equational reasoning through canonical simplification (rewriting theory) and proofs by induction (following Boyer and Moore successful integration of primitive recursive arithmetic within the LISP programming language). The special case of Horn clauses gave rise to a new paradigm of non-deterministic programming, called Logic Programming, developing later into Constraint Programming, blurring further the scope of logic. In order to study knowledge acquisition, researchers in artificial intelligence and computational linguistics studied exotic versions of modal logics such as Montague intentional logic, epistemic logic, dynamic logic or hybrid logic. Some others tried to capture common sense, and modeled the revision of beliefs with so-called non-monotonic logics. For the careful crafstmen of mathematical logic, this was the final outrage, and Girard gave his anathema to such “montres à moutardes”.

APA, Harvard, Vancouver, ISO, and other styles

21

Kołodziejczyk, Leszek Aleksander. "Truth definitions in finite models." Journal of Symbolic Logic 69, no. 1 (March 2004): 183–200. http://dx.doi.org/10.2178/jsl/1080938836.

Full text

Abstract:

AbstractThe paper discusses the notion of finite model truth definitions (or FM-truth definitions), introduced by M. Mostowski as a finite model analogue of Tarski's classical notion of truth definition.We compare FM-truth definitions with Vardi's concept of the combined complexity of logics, noting an important difference: the difficulty of defining FM-truth for a logic does not depend on the syntax of , as long as it is decidable. It follows that for a natural there exist FM-truth definitions whose evaluation is much easier than the combined complexly of would suggest.We apply the general theory to give a complexity-theoretical characterization of the logics for which the classes (prenex classes of higher order logics) define FM-truth. For any d ≥ 2, m ≥ 1 we construct a family of syntactically defined fragments of which satisfy this characterization. We also use the classes to give a refinement of known results on the complexity classes captured by .We close with a few simple corollaries, one of which gives a sufficient condition for the existence, given a vocabulary σ, of a fixed number k such that model checking for all first order sentences over σ can be done in deterministic time nk.

APA, Harvard, Vancouver, ISO, and other styles

22

Okada, Mitsuhiro. "A uniform semantic proof for cut-elimination and completeness of various first and higher order logics." Theoretical Computer Science 281, no. 1-2 (June 2002): 471–98. http://dx.doi.org/10.1016/s0304-3975(02)00024-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

23

Conrath-Hargreaves, Annemarie, and Sonja Wüstemann. "Multiple institutional logics and their impact on accounting in higher education." Accounting, Auditing & Accountability Journal 32, no. 3 (March 18, 2019): 782–810. http://dx.doi.org/10.1108/aaaj-08-2017-3095.

Full text

Abstract:

Purpose The purpose of this paper is to explore how an Higher Education Institution’s (HEI) choice of undergoing a voluntary reorganisation, motivated by its own interest of increasing its autonomy, whilst also having to satisfy the government in order to maintain the level of public funding, impacts on the HEI’s accounting. Design/methodology/approach The paper draws on the institutional logics perspective to present a single case study of a German HEI that chose to be reorganised from a public into a foundation university. Data were obtained using multiple data collection methods. Findings The findings suggest that organisational characteristics, which act as filters for institutional logics, play an important role for HEIs’ ability to increase not only their de jure, but also their de facto autonomy through self-motivated, rather than government imposed, reform processes. Research limitations/implications The paper is based on a single case study in a country-specific context, limiting the empirical generalisability of the findings. Originality/value Germany is not only one of the main nations exporting higher education, but its economy has also been recognised for its stability and development over the last decades. Nevertheless, Germany struggles in its transition to become a knowledge-based economy. Yet, research has so far tended to neglect educational reforms in Continental European countries, such as Germany. By addressing this gap in the literature, this paper is among the first to explore how reform processes shape accounting in German HEIs.

APA, Harvard, Vancouver, ISO, and other styles

24

Gürses, Serdal, and Ali Danışman. "Keeping institutional logics in arm’s length: emerging of rogue practices in a gray zone of everyday work life in healthcare." Journal of Professions and Organization 8, no. 2 (July 1, 2021): 128–67. http://dx.doi.org/10.1093/jpo/joab004.

Full text

Abstract:

Abstract We set out to explore the practice-level cognitive structures and associated practices characterizing the daily routine work of physicians by conducting a qualitative study in the Turkish healthcare field, in which a recent government-led healthcare reform was implemented causing logic multiplicity. Contrary to the accumulated knowledge in institutional logics literature, a bulk of which suggests that actors craft and enact various practices in managing plural and at times conflicting institutional templates strictly within the confines of higher order societal logics, this study shows that while ground level actors may not exercise complete freedom and maneuverability in relation to pre-established social structures, they do incorporate unconventional schemas of action; namely rogue practices, into their embodied practical activity, which over time become routinized in their day-to-day work lives. Unraveling the dynamics of micro-level practices of highly professionalized ground level actors as they pertain to atypical logical orientations substantially advances our understanding of the unknown or unseen side of how and under which conditions certain or various combinations of institutional logics are employed during day-to-day activities.

APA, Harvard, Vancouver, ISO, and other styles

25

KIRCHNER, DANIEL, CHRISTOPH BENZMÜLLER, and EDWARD N. ZALTA. "MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY." Review of Symbolic Logic 13, no. 1 (July 12, 2019): 206–18. http://dx.doi.org/10.1017/s1755020319000297.

Full text

Abstract:

AbstractPrincipia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory (inspired by ideas of Ernst Mally, formalized by Zalta) that distinguishes between ordinary and abstract objects.This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms is simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics.Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics.

APA, Harvard, Vancouver, ISO, and other styles

26

Chlipala, Adam. "Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)." Proceedings of the ACM on Programming Languages 5, ICFP (August 22, 2021): 1–28. http://dx.doi.org/10.1145/3473599.

Full text

Abstract:

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.

APA, Harvard, Vancouver, ISO, and other styles

27

Schmidt, Dennis R. "Peremptory law, global order, and the normative boundaries of a pluralistic world." International Theory 8, no. 2 (May 5, 2016): 262–96. http://dx.doi.org/10.1017/s175297191600004x.

Full text

Abstract:

This article develops a socio-legal approach to theorizing the construction of peremptory norms in international relations. It argues that due to its focus on formalism and abstract notions of rights, traditional legal treatments have failed to acknowledge the socially constructed nature of higher order norms. To address this shortcoming, the article transfers the concept ofjus cogensinto the realm of International Relations. Drawing on insights from constructivism and English School theory, it situates law in the context of society and conceptualizesjus cogensas part of international society’s constitutional structure. Proceeding from the assumption that the content and identity ofjus cogensdepends on the normative character of international society, the article then assesses two possible ‘normative logics’ through which the peremptory status of a norm may be generated. It rejects a solidarist logic, which sees universal norms as the manifestation of cosmopolitan ideas about inalienable rights. Instead, it argues for a pluralist approach to ethics and order that depictsjus cogensas key to the development of international society towards a social site marked by diversity and respect for difference.

APA, Harvard, Vancouver, ISO, and other styles

28

Niestegge, Gerd. "Conditional Probability, Three-Slit Experiments, and the Jordan Algebra Structure of Quantum Mechanics." Advances in Mathematical Physics 2012 (2012): 1–20. http://dx.doi.org/10.1155/2012/156573.

Full text

Abstract:

Most quantum logics do not allow for a reasonable calculus of conditional probability. However, those ones which do so provide a very general and rich mathematical structure, including classical probabilities, quantum mechanics, and Jordan algebras. This structure exhibits some similarities with Alfsen and Shultz's noncommutative spectral theory, but these two mathematical approaches are not identical. Barnum, Emerson, and Ududec adapted the concept of higher-order interference, introduced by Sorkin in 1994, into a general probabilistic framework. Their adaption is used here to reveal a close link between the existence of the Jordan product and the nonexistence of interference of third or higher order in those quantum logics which entail a reasonable calculus of conditional probability. The complete characterization of the Jordan algebraic structure requires the following three further postulates: a Hahn-Jordan decomposition property for the states, a polynomial functional calculus for the observables, and the positivity of the square of an observable. While classical probabilities are characterized by the absence of any kind of interference, the absence of interference of third (and higher) order thus characterizes a probability calculus which comes close to quantum mechanics but still includes the exceptional Jordan algebras.

APA, Harvard, Vancouver, ISO, and other styles

29

BARBERO, FAUSTO. "SOME OBSERVATIONS ABOUT GENERALIZED QUANTIFIERS IN LOGICS OF IMPERFECT INFORMATION." Review of Symbolic Logic 12, no. 3 (April 12, 2019): 456–86. http://dx.doi.org/10.1017/s1755020319000145.

Full text

Abstract:

AbstractWe analyse the two definitions of generalized quantifiers for logics of dependence and independence that have been proposed by F. Engström, comparing them with a more general, higher order definition of team quantifier. We show that Engström’s definitions (and other quantifiers from the literature) can be identified, by means of appropriate lifts, with special classes of team quantifiers. We point out that the new team quantifiers express a quantitative and a qualitative component, while Engström’s quantifiers only range over the latter. We further argue that Engström’s definitions are just embeddings of the first-order generalized quantifiers into team semantics, and fail to capture an adequate notion of team-theoretical generalized quantifier, save for the special cases in which the quantifiers are applied to flat formulas. We also raise several doubts concerning the meaningfulness of the monotone/nonmonotone distinction in this context. In the appendix we develop some proof theory for Engström’s quantifiers.

APA, Harvard, Vancouver, ISO, and other styles

30

Jacinto, Bruno. "Necessitism, Contingentism, and Theory Equivalence." Bulletin of Symbolic Logic 27, no. 2 (June 2021): 217–18. http://dx.doi.org/10.1017/bsl.2021.25.

Full text

Abstract:

AbstractNecessitism, Contingentism, and Theory Equivalence is a dissertation on issues in higher-order modal metaphysics. Consider a modal higher-order language with identity in which the universal quantifier is interpreted as expressing (unrestricted) universal quantification and the necessity operator is interpreted as expressing metaphysical necessity. The main question addressed in the dissertation concerns the correct theory formulated in this language. A different question that also takes centre stage in the dissertation is what it takes for theories to be equivalent.The whole dissertation consists of an extended argument in defence of the (joint) truth of two seemingly inconsistent higher-order modal theories, specifically: 1.Plantingan Moderate Contingentism, a theory based on Plantinga’s [1] modal metaphysics that is committed to, among other things, the contingent being of some individuals and the necessary being of all possible higher-order entities;2.Williamsonian Thorough Necessitism, a theory advocated by Williamson [3] which is committed to, among other things, the necessary being of every possible individual as well as of every possible higher-order entity.Part of the case for these theories’ joint truth relies on defences of the following metaphysical theses: (i) Thorough Serious Actualism, the thesis that no things could have been related while being nothing, and (ii) Higher-Order Necessitism, the thesis that necessarily, every higher-order entity is necessarily something. It is shown that Thorough Serious Actualism and Higher-Order Necessitism are both implicit commitments of very weak logical theories. The defence of Higher-Order Necessitism constitutes a powerful challenge to Stalnaker’s [2] Thorough Contingentism, a theory committed to, among other things, the view that there could have been some individuals as well as some entities of any higher-order that could have been nothing.In the dissertation it is argued that Plantingan Moderate Contingentism and Williamsonian Thorough Necessitism are in fact equivalent, even if they appear to be jointly inconsistent. The case for this claim relies on the Synonymy account, a novel account of theory equivalence developed and defended in the dissertation. According to this account, theories are equivalent just in case they have the same commitments and conception of logical space.By way of defending the Synonymy account’s adequacy, the account is applied to the debate between noneists, proponents of the view that some things do not exist, and Quineans, proponents of the view that to exist just is to be some thing. The Synonymy account is shown to afford a more nuanced and better understanding of that debate by revealing that what noneists and Quineans are really disagreeing about is what expressive resources are available to appropriately describe the world.By coupling a metatheoretical result with tools from the philosophy of language, it is argued that Plantingan Moderate Contingentism and Williamsonian Thorough Necessitism are synonymous theories, and so, by the lights of the Synonymy account, equivalent. Given the defence of their extant commitments made in the dissertation, it is concluded that Plantingan Moderate Contingentism and Williamsonian Thorough Necessitism are both correct. A corollary of this result is that the dispute between Plantingans and Williamsonians is, in an important sense, merely verbal. For if two theories are equivalent, then they “require the same of the world for their truth.”Thus, the results of the dissertation reveal that if one speaks as a Plantingan while advocating Plantingan Moderate Contingentism, or as a Williamsonian while advocating Williamsonian Thorough Necessitism, then one will not go wrong. Notwithstanding, one will still go wrong if one speaks as a Plantingan while advocating Williamsonian Thorough Necessitism, or as a Williamsonian while advocating Plantingan Moderate Contingentism.On the basis of a conception of the individual constants and predicates of second-order modal languages as strongly Millian, i.e., as having actually existing entities as their semantic values, in the appendix are presented second-order modal logics consistent with Stalnaker’s Thorough Contingentism. Furthermore, it is shown there that these logics are strong enough for applications of higher-order modal logic in mathematics, a result that constitutes a reply to an argument to the contrary by Williamson [3]. Finally, these logics are proven to be complete relative to particular “thoroughly contingentist” classes of models.

APA, Harvard, Vancouver, ISO, and other styles

31

Larsen, Katarina. "Managing the complexity of centres of excellence: accommodating diversity in institutional logics." Tertiary Education and Management 26, no. 3 (December 6, 2019): 295–310. http://dx.doi.org/10.1007/s11233-019-09053-w.

Full text

Abstract:

AbstractThis article discusses how Centres of Excellence (CoE) and the existence of several logics in these centres can contribute to the differentiation of the strategic profiles of universities. The study sees research centres as a way to organize research activities in Higher Education Institutions (HEIs) in order to target both excellence but also societal challenges through focused thematic research. It reveals how societal challenges and their interpretation by these centres contribute to the differentiation of the strategic profiles of universities. Studies of centres of excellence programs in Sweden and Japan reveal differences in how their mission is formulated for relevance and excellence. The results indicate that contrasting missions of HEIs are accommodated through the dual logics of these centres relating both to autonomy and industry collaboration. The study shows that long-term funding gives these centres flexibility to set the agenda and focus on their strategic core activities. In other words, a logic of autonomy guides their strategic choices of research activities over the long-run as well as collaborators. Nevertheless, these centres are also developing strategies to cope with dilemmas stemming from the excellence-relevance and evaluation templates that emerge in the nexus of their collaborative ties with industry, government and universities.

APA, Harvard, Vancouver, ISO, and other styles

32

Diab, Ahmed, and Ahmed Aboud. "The interplay between ideological resistance and management control: an Egyptian case study." Journal of Accounting in Emerging Economies 9, no. 2 (May 7, 2019): 208–36. http://dx.doi.org/10.1108/jaee-07-2017-0070.

Full text

Abstract:

Purpose This study explores the relationship between institutional logics and workers’ agency in business organisations. The purpose of this paper is to explain management control in a complex setting of workers’ resistance and institutional multiplicity and complexity. Exploring the inherent political volatility at the macro level, the work also investigates the political aspects of economic organisations and the intermediary role of individuals who deal with these institutions. Design/methodology/approach Theoretically, the study triangulates institutional logics and labour process theories, linking higher-order institutions with mundane labour practices observed in the case study. Methodologically, the study adopts a post-positivistic case study approach. Empirical data were solicited in a village community, where sugar beet farming and processing constitutes the main economic activity underlying its livelihood. Data were collected through a triangulation of interviews, documents and observations. Findings The study concludes that, especially in LDCs agro-manufacturing settings, economic and societal institutions play a central role in the mobilisation of labour resistance. Control can be effectively practiced, and be resisted, through such economic and social systems. This study affirms the influence of institutional logics on individuals’ agency and subjectivity. Originality/value The study contributes to literature by investigating the relationship between subalterns’ agency and institutional logics in a traditional political and communal context, in contrast to the highly investigated western contexts; and providing a definition of management control based on the prevalent institutional logics in the field.

APA, Harvard, Vancouver, ISO, and other styles

33

Diab, Ahmed, and Abdelmoneim Bahyeldin Mohamed Metwally. "Institutional complexity and CSR practices: evidence from a developing country." Journal of Accounting in Emerging Economies 10, no. 4 (September 17, 2020): 655–80. http://dx.doi.org/10.1108/jaee-11-2019-0214.

Full text

Abstract:

PurposeThe study aims to investigate the appearance of corporate social and environmental responsibility (CSER) practices in a context where economic, communal and political institutions are highly central and competing with each other.Design/methodology/approachTheoretically, the study draws upon the institutional logics perspective and the theoretical concepts of logics centrality and compatibility to understand how higher-order institutions interact with mundane CSER practices observed at the case company's micro level. Empirical data were solicited in an Egyptian village community, where fishing, agriculture and especially salt production constitute the main economic activities underlying its livelihood. A combination of interviews, informal conversations, observations and documents solicits the required data.FindingsThereby, this study presents an inclusive view of CSER as practiced in developing countries, which is based not only on rational economic perspectives – as is the case in developed and stabilised contexts – but also on social, familial and political aspects that are central to the present complex institutional environment.Originality/valueThe reported findings in this study highlight the role of non-economic (societal) logics in understating CSER in African developing nations.

APA, Harvard, Vancouver, ISO, and other styles

34

Hodes, Harold. "Cardinality logics. Part II: Definability in languages based on ‘exactly’." Journal of Symbolic Logic 53, no. 3 (September 1988): 765–84. http://dx.doi.org/10.2307/2274570.

Full text

Abstract:

This paper continues the project initiated in [5]: a model-theoretic study of the concept of cardinality within certain higher-order logics. As recommended by an editor of this Journal, I will digress to say something about the project's motivation. Then I will review some of the basic definitions from [5]; for unexplained notation the reader should consult [5].The syntax of ordinary usage (with respect to the construction of arguments as well as the construction of individual sentences) makes it natural to classify numerals and expressions of the form ‘the number of F's’ as singular terms, expressions like ‘is prime’ or ‘is divisible by’ as predicates of what Frege called “level one”, and expressions like ‘for some natural number’ as first-order quantifier-phrases. From this syntatic classification, it is a short step—so short as to be frequently unnoticed—to a semantic thesis: that such expressions play the same sort of semantic role as is played by the paradigmatic (and nonmathematical) members of these lexical classes. Thus expressions of the first sort are supposed to designate objects (in post-Fregean terms, entities of type 0), those of the second sort to be true or false of tuples of objects, and those of the third sort to quantify over objects. All this may be summed up in Frege's dictum: “Numbers are objects.”

APA, Harvard, Vancouver, ISO, and other styles

35

Diab, Ahmed Abdelnaby Ahmed, and Abdelmoneim Bahyeldin Mohamed Metwally. "Institutional ambidexterity and management control." Qualitative Research in Accounting & Management 16, no. 3 (August 5, 2019): 373–402. http://dx.doi.org/10.1108/qram-08-2017-0081.

Full text

Abstract:

Purpose The purpose of this study is to investigate in depth how an organisation is able to achieve its economic objectives in a situation of institutional complexity through being institutionally dexterous. The study also investigates how this is done through overriding formal controls and concentrating on socio-political and communal-based controls. Design/methodology/approach Theoretically, the study draws on the perspectives of institutional complexity and ambidexterity to link higher-order institutions with mundane labour control practices observed at the micro level of the case company. Methodologically, the study adopts an interpretive – case study – approach. Empirical data were solicited in an Egyptian village community, where sugar beet farming and processing constitutes the main economic activity underlying its livelihood. Data were collected through a triangulation of interviews, documents and observations. Findings The study concludes that, especially in socio-political contexts such as Egypt, the organisational environment can better be understood and perceived as institutionally complex situation. To manage such complexity and to effectively meet its economic objectives, the organisation needs to be institutionally dextrous. Thereby, this study presents an inclusive view of management control (MC) which is based not only on rational economic practices, but also on social, religious and political aspects that are central to this institutional environment. Originality/value The study contributes to MC and logics literature in a number of respects. It extends the institutional logics debate by illustrating that logics get re-institutionalised by the “place” through its cultural, political and communal identities that filter logics’ complexities to different ends. Further, it extends the cultural political economy of MC by illustrating that MC in socio-political settings is also an operational manifestation of the logics prevailing in the context. These logics produced an informal MC system that dominated the formal known MCs.

APA, Harvard, Vancouver, ISO, and other styles

36

Aschieri, Federico, Stefan Hetzl, and Daniel Weller. "Expansion trees with cut." Mathematical Structures in Computer Science 29, no. 8 (September 2019): 1009–29. http://dx.doi.org/10.1017/s0960129519000069.

Full text

Abstract:

AbstractHerbrand’s theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logics by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller’s expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas.In this paper, we present a new syntactic approach that directly extends Miller’s expansion trees by cuts and also covers non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and shows that it is weakly normalizing.

APA, Harvard, Vancouver, ISO, and other styles

37

Carrington, Thomas, Tobias Johansson, Gustav Johed, and Peter Öhman. "An Empirical Test of the Hierarchical Construct of Professionalism and Managerialism in the Accounting Profession." Behavioral Research in Accounting 25, no. 2 (May 1, 2013): 1–20. http://dx.doi.org/10.2308/bria-50511.

Full text

Abstract:

ABSTRACT: Research into the tension between professionalism and commercialism in the accounting profession is inconclusive and warrants greater attention. How to conceptualize and measure these constructs are thus pressing concerns. Using questionnaire data from 1,646 auditors in Sweden, and applying confirmatory factor analysis and structural regression models within a structural equation modeling framework to a measurement model developed by Suddaby et al. (2009), we find little empirical evidence for the existence of the two logics of professionalism and managerialism (i.e., commercialism) as two higher-order latent constructs shared by auditors. However, we find that two sub-elements of the proposed higher-order constructs do discriminate between each other in a way that could indicate two exclusive value statements in the accounting profession connected to the professionalism–commercialism tension; these are the respective emphasis on independence enforcement and client commitment.

APA, Harvard, Vancouver, ISO, and other styles

38

Wilson, Steven R., Kai Kuang, Elizabeth A. Hintz, and Patrice M. Buzzanell. "Developing and Validating the Communication Resilience Processes Scale." Journal of Communication 71, no. 3 (April 19, 2021): 478–513. http://dx.doi.org/10.1093/joc/jqab013.

Full text

Abstract:

Abstract According to the communication theory of resilience (CTR; P. M. Buzzanell, 2010), people reintegrate from disruptive events and construct a new normal through five interrelated processes: (a) crafting normalcy; (b) affirming identity anchors; (c) maintaining/using communication networks; (d) constructing alternative logics; and (e) foregrounding productive action while backgrounding negative emotions. Enacting these processes creates tensions between continuity and change. This article develops a Communication Resilience Processes Scale (CRPS) to assess CTR processes in response to a variety of disruptive events. Items were created and refined via a scale development study with feedback from expert raters. Studies 2 and 3 offer initial support for the 32-item CRPS’ reliability and convergent, divergent, and predictive validity. Models in which the five CTR processes are subsumed by a single, higher-order resilience factor versus two higher-order interrelated factors (continuity and change) are compared. Future directions for exploring continuity/change tensions and identifying CTR boundary conditions are discussed.

APA, Harvard, Vancouver, ISO, and other styles

39

BOVE, ANA, ALEXANDER KRAUSS, and MATTHIEU SOZEAU. "Partiality and recursion in interactive theorem provers – an overview." Mathematical Structures in Computer Science 26, no. 1 (November 10, 2014): 38–88. http://dx.doi.org/10.1017/s0960129514000115.

Full text

Abstract:

The use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalizing mathematics is becoming more common and feasible in practice. However, most mature theorem provers lack a direct treatment of partial and general recursive functions; overcoming this weakness has been the objective of intensive research during the last decades. In this article, we review several techniques that have been proposed in the literature to simplify the formalization of partial and general recursive functions in interactive theorem provers. Moreover, we classify the techniques according to their theoretical basis and their practical use. This uniform presentation of the different techniques facilitates the comparison and highlights their commonalities and differences, as well as their relative advantages and limitations. We focus on theorem provers based on constructive type theory (in particular, Agda and Coq) and higher-order logic (in particular Isabelle/HOL). Other systems and logics are covered to a certain extent, but not exhaustively. In addition to the description of the techniques, we also demonstrate tools which facilitate working with the problematic functions in particular theorem provers.

APA, Harvard, Vancouver, ISO, and other styles

40

Bruce, Kim, Johan van Benthem, and Kees Doets. "Higher-order Logic." Journal of Symbolic Logic 54, no. 3 (September 1989): 1090. http://dx.doi.org/10.2307/2274769.

Full text

APA, Harvard, Vancouver, ISO, and other styles

41

Di Pinto, Floriana, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, and Riccardo Rosati. "Acquiring Ontology Axioms through Mappings to Data Sources." Future Internet 11, no. 12 (December 13, 2019): 260. http://dx.doi.org/10.3390/fi11120260.

Full text

Abstract:

Although current languages used in ontology-based data access (OBDA) systems allow for mapping source data to instances of concepts and relations in the ontology, several application domains need more flexible tools for inferring knowledge from data, which are able to dynamically acquire axioms about new concepts and relations directly from the data. In this paper we introduce the notion of mapping-based knowledge base (MKB) to formalize the situation where both the extensional and the intensional level of the ontology are determined by suitable mappings to a set of data sources. This allows for making the intensional level of the ontology as dynamic as the extensional level traditionally is. To do so, we resort to the meta-modeling capabilities of higher-order description logics, in particular the description logic Hi ( DL-Lite R ) , which allows seeing concepts and relations as individuals, and vice versa. The challenge in this setting is to design efficient algorithms for answering queries posed to MKBs. Besides the definition of MKBs, our main contribution is to prove that answering instance queries posed to MKBs expressed in Hi ( DL-Lite R ) can be done efficiently.

APA, Harvard, Vancouver, ISO, and other styles

42

Došen, Kosta. "Sequent-systems for modal logic." Journal of Symbolic Logic 50, no. 1 (March 1985): 149–68. http://dx.doi.org/10.2307/2273797.

Full text

Abstract:

AbstractThe purpose of this work is to present Gentzen-style formulations of S5 and S4 based on sequents of higher levels. Sequents of level 1 are like ordinary sequents, sequents of level 2 have collections of sequents of level 1 on the left and right of the turnstile, etc. Rules for modal constants involve sequents of level 2, whereas rules for customary logical constants of first-order logic with identity involve only sequents of level 1. A restriction on Thinning on the right of level 2, which when applied to Thinning on the right of level 1 produces intuitionistic out of classical logic (without changing anything else), produces S4 out of S5 (without changing anything else).This characterization of modal constants with sequents of level 2 is unique in the following sense. If constants which differ only graphically are given a formally identical characterization, they can be shown inter-replaceable (not only uniformly) with the original constants salva provability. Customary characterizations of modal constants with sequents of level 1, as well as characterizations in Hilbert-style axiomatizations, are not unique in this sense. This parallels the case with implication, which is not uniquely characterized in Hilbert-style axiomatizations, but can be uniquely characterized with sequents of level 1.These results bear upon theories of philosophical logic which attempt to characterize logical constants syntactically. They also provide an illustration of how alternative logics differ only in their structural rules, whereas their rules for logical constants are identical.

APA, Harvard, Vancouver, ISO, and other styles

43

Forster, Thomas. "A Consistent Higher-Order Theory Without a (Higher-Order) Model." Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 35, no. 5 (1989): 385–86. http://dx.doi.org/10.1002/malq.19890350502.

Full text

APA, Harvard, Vancouver, ISO, and other styles

44

Puga, Leila Z., and Newton C. A. Da Costa. "Sobre a lógica deôntica não-clássica." Crítica (México D. F. En línea) 19, no. 55 (December 10, 1987): 19–37. http://dx.doi.org/10.22201/iifs.18704905e.1987.639.

Full text

Abstract:

Our starting point, in this basically expository paper, is the study of a classical system of deontic propositional logic, classical in the sense that it constitutes an extension of the classical propositional calculus. It is noted, then, that the system excludes ab initio the possibility of the existence of real moral dilemmas (contradictory obligations and prohibitions), and also can not cope smoothly with the so-called prima facie moral dilemmas. So, we develop a non-classical, paraconsistent system of propositional deontic logic which is compatible with such dilemmas, real or prima facie. In our paraconsistent system one can handle them neatly, in particular one can directly investigate their force, operational meaning, and the most important consequences of their acceptance as not uncommon moral facts. Of course, we are conscious that other procedures for dealing with them are at hand, for example by the weakening of the specific deontic axioms. It is not argued that our procedure is the best, at least as regards the present state of the issue. We think only that owing, among other reasons, to the circumstance that the basic ethical concepts are intrinsically vague, it seems quite difficult to get rid of moral dilemmas and of moral deadlocks in general. Apparently this speaks in favour of a paraconsistent approach to ethics. At any rate, a final appraisal of the possible solutions to the problem of dilemmas and deadlocks, if there is one, constitutes a matter of ethical theory and not only of logic. On the other hand, the paraconsistency stance looks likely to be relevant also in the field of legal logic. It is shown, in outline, that the systems considered are sound and complete, relative to a natural semantics. All results of this paper can be extended to first-order and to higher-order logics. Such extensions give rise to the question of the transparency (or oppacity) of the deontic contexts. As we shall argue in forthcoming articles, they normally are transparent. [L.Z.P., N.C.A. da C.] (PDF en portugués)

APA, Harvard, Vancouver, ISO, and other styles

45

Davis, Alexander K. "Toward Exclusion through Inclusion: Engendering Reputation with Gender-Inclusive Facilities at Colleges and Universities in the United States, 2001-2013." Gender & Society 32, no. 3 (April 4, 2018): 321–47. http://dx.doi.org/10.1177/0891243218763056.

Full text

Abstract:

Ample sociological evidence demonstrates that binary gender ideologies are an intractable part of formal organizations and that transgender issues tend to be marginalized by a wide range of social institutions. Yet, in the last 15 years, more than 200 colleges and universities have attempted to ameliorate such realities by adopting gender-inclusive facilities in which students of any gender can share residential and restroom spaces. What cultural logics motivate these transformations? How can their emergence be reconciled with the difficulty of altering the gender order? Using an original sample of 2,036 campus newspaper articles, I find that support for inclusive facilities frames such spaces as a resource through which an institution can claim improved standing in the field of higher education. This process of engendering reputation allows traditional gender separation in residential arrangements to be overcome, but it also situates institutional responsiveness to transgender issues as a means of enhancing a college or university’s public prestige. This, in turn, produces novel status systems in the field of higher education—albeit ones that perpetuate familiar forms of institutional and cultural exclusion.

APA, Harvard, Vancouver, ISO, and other styles

46

Audenaert, Pieter. "The Higher-Order-Logic Formath." Bulletin of the Belgian Mathematical Society - Simon Stevin 15, no. 2 (May 2008): 335–67. http://dx.doi.org/10.36045/bbms/1210254829.

Full text

APA, Harvard, Vancouver, ISO, and other styles

47

Charalambidis, Angelos, Konstantinos Handjopoulos, Panagiotis Rondogiannis, and William W. Wadge. "Extensional Higher-Order Logic Programming." ACM Transactions on Computational Logic 14, no. 3 (August 2013): 1–40. http://dx.doi.org/10.1145/2499937.2499942.

Full text

APA, Harvard, Vancouver, ISO, and other styles

48

Czajka, Łukasz. "Higher-Order Illative Combinatory Logic." Journal of Symbolic Logic 78, no. 3 (September 2013): 837–72. http://dx.doi.org/10.2178/jsl.7803080.

Full text

Abstract:

AbstractWe show a model construction for a system of higher-order illative combinatory logic thus establishing its strong consistency. We also use a variant of this construction to provide a complete embedding of first-order intuitionistic predicate logic with second-order propositional quantifiers into the system of Barendregt, Bunder and Dekkers, which gives a partial answer to a question posed by these authors.

APA, Harvard, Vancouver, ISO, and other styles

49

Cropper, Andrew, Rolf Morel, and Stephen Muggleton. "Learning higher-order logic programs." Machine Learning 109, no. 7 (December 3, 2019): 1289–322. http://dx.doi.org/10.1007/s10994-019-05862-7.

Full text

Abstract:

AbstractA key feature of inductive logic programming is its ability to learn first-order programs, which are intrinsically more expressive than propositional programs. In this paper, we introduce techniques to learn higher-order programs. Specifically, we extend meta-interpretive learning (MIL) to support learning higher-order programs by allowing for higher-order definitions to be used as background knowledge. Our theoretical results show that learning higher-order programs, rather than first-order programs, can reduce the textual complexity required to express programs, which in turn reduces the size of the hypothesis space and sample complexity. We implement our idea in two new MIL systems: the Prolog system $$\text {Metagol}_{ho}$$ Metagol ho and the ASP system $$\text {HEXMIL}_{ho}$$ HEXMIL ho . Both systems support learning higher-order programs and higher-order predicate invention, such as inventing functions for and conditions for . We conduct experiments on four domains (robot strategies, chess playing, list transformations, and string decryption) that compare learning first-order and higher-order programs. Our experimental results support our theoretical claims and show that, compared to learning first-order programs, learning higher-order programs can significantly improve predictive accuracies and reduce learning times.

APA, Harvard, Vancouver, ISO, and other styles

50

Hetzl, Stefan, Alexander Leitsch, and Daniel Weller. "CERES in higher-order logic." Annals of Pure and Applied Logic 162, no. 12 (December 2011): 1001–34. http://dx.doi.org/10.1016/j.apal.2011.06.005.

Full text

APA, Harvard, Vancouver, ISO, and other styles

Journal articles on the topic 'Higher order logics'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles