JournalTOCs

Journal of Applied Logic

Subscription journal
ISSN (Print) 1570-8683
Published by Elsevier

[2564 journals]

Ordered domain algebras
- Abstract: Publication date: Available online 2 May 2013
  Source:Journal of Applied Logic
  Author(s): Robin Hirsch , Szabolcs Mikulás
  We give a finite axiomatisation to representable ordered domain algebras and show that finite algebras are representable on finite bases.
  
  PubDate: 2013-05-03T02:08:16Z
A model of type theory in simplicial sets
- Abstract: Publication date: Available online 24 April 2013
  Source:Journal of Applied Logic
  Author(s): T. Streicher
  ???
  
  PubDate: 2013-04-29T02:07:39Z
Editorial Board
- Abstract: Publication date: June 2013
  Source:Journal of Applied Logic, Volume 11, Issue 2
  
  PubDate: 2013-04-25T02:07:34Z
Skew Lattices and Binary Operations on Functions
- Abstract: Available online 30 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  A recent study of the override and update operations defined on sets of partial functions placed both operations within the algebraic context of a certain variety of algebras. We show the latter to be term equivalent to the variety of right-handed skew Boolean algebras. Both operations are then studied within the broader context of skew lattices with an eye towards achieving greater insight into their joint algebraic behavior. A decision procedure is given to determine whether an equation in both operations holds for all sets of partial functions.
  
  PubDate: 2013-04-01T02:09:36Z
Simulative belief logic
- Abstract: Available online 21 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  The ability of ascribing beliefs to others is crucial for human beings to explain and understand each other. Belief ascription has been studied intensively in philosophy and cognitive science. In this paper, we propose a formal framework for belief ascription by simulation. An agent first acquires information about another agentʼs beliefs by communication. She then inputs the information into her own belief system to generate more beliefs, which she will ascribe to the other agent. In this way, the agent uses her own as a model of others. We present a modal belief logic, which contains private announcement operators for agentsʼ communication, and simulative belief operators for beliefs ascribed to others. We give a complete axiomatic system for the logic.
  
  PubDate: 2013-03-24T03:07:29Z
Modal definability of first-order formulas with free variables and query answering
- Abstract: Available online 20 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  We present an algorithmically efficient criterion of modal definability for first-order existential conjunctive formulas with several free variables. Then we apply it to establish modal definability of some family of first-order ∀∃-formulas. Finally, we use our definability results to show that, in any expressive description logic, the problem of answering modally definable conjunctive queries is polynomially reducible to the problem of knowledge base consistency.
  
  PubDate: 2013-03-24T03:07:29Z
A QBF-based formalization of abstract argumentation semantics
- Abstract: Available online 21 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  We introduce a unified logical theory, based on signed theories and Quantified Boolean Formulas (QBFs) that can serve as the basis for representing and computing various argumentation-based decision problems. It is shown that within our framework we are able to model, in a simple and modular way, a wide range of semantics for abstract argumentation theory. This includes complete, grounded, preferred, stable, semi-stable, stage, ideal and eager semantics. Furthermore, our approach is purely logical, making for instance decision problems like skeptical and credulous acceptance of arguments simply a matter of entailment and satisfiability checking. The latter may be verified by off-the-shelf QBF-solvers.
  
  PubDate: 2013-03-24T03:07:29Z
An observation on Carnapʼs Continuum and Stochastic Independencies
- Abstract: Available online 18 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  We characterize those identities and independencies which hold for all probability functions on a unary language satisfying the Principle of Atom Exchangeability. We then show that if this is strengthen to the requirement that Johnsonʼs Sufficientness Principle holds, thus giving Carnapʼs Continuum of inductive methods for languages with at least two predicates, then new and somewhat inexplicable identities and independencies emerge, the latter even in the case of Carnapʼs Continuum for the language with just a single predicate.
  
  PubDate: 2013-03-20T03:07:19Z
From Bayesian epistemology to inductive logic
- Abstract: Available online 18 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  Inductive logic admits a variety of semantics [7, Part 1]. This paper develops semantics based on the norms of Bayesian epistemology [16, Chapter7]. §1 introduces the semantics and then, in $ 2, the paper explores methods for drawing inferences in the resulting logic and compares the methods of this paper with the methods of Barnett and Paris [2]. §3 then evaluates this Bayesian inductive logic in the light of four traditional critiques of inductive logic, arguing (i) that it is language independent in a key sense, (ii) that it admits connections with the Principle of Indifference but these connections do not lead to paradox, (iii) that it can capture the phenomenon of learning from experience, and (iv) that while the logic advocates scepticism with regard to some universal hypotheses, such scepticism is not problematic from the point of view of scientific theorising.
  
  PubDate: 2013-03-20T03:07:19Z
Confirmation as partial entailment: A representation theorem in inductive logic
- Abstract: Available online 18 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  The most prominent research program in inductive logic – here just labelled The Program, for simplicity – relies on probability theory as its main building block and aims at a proper generalization of deductive-logical relations by a theory of partial entailment. We prove a representation theorem by which a class of ordinally equivalent measures of inductive support or confirmation is singled out as providing a uniquely coherent way to work out these two major sources of inspiration of The Program.
  
  PubDate: 2013-03-20T03:07:19Z
Probabilities on Sentences in an Expressive Logic
- Abstract: Available online 18 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  Automated reasoning about uncertain knowledge has many applications. One difficulty when developing such systems is the lack of a completely satisfactory integration of logic and probability. We address this problem directly. Expressive languages like higher-order logic are ideally suited for representing and reasoning about structured knowledge. Uncertain knowledge can be modeled by using graded probabilities rather than binary truth-values. The main technical problem studied in this paper is the following: Given a set of sentences, each having some probability of being true, what probability should be ascribed to other (query) sentences? A natural wish-list, among others, is that the probability distribution (i) is consistent with the knowledge base, (ii) allows for a consistent inference procedure and in particular (iii) reduces to deductive logic in the limit of probabilities being 0 and 1, (iv) allows (Bayesian) inductive reasoning and (v) learning in the limit and in particular (vi) allows confirmation of universally quantified hypotheses/sentences. We translate this wish-list into technical requirements for a prior probability and show that probabilities satisfying all our criteria exist. We also give explicit constructions and several general characterizations of probabilities that satisfy some or all of the criteria and various (counter) examples. We also derive necessary and sufficient conditions for extending beliefs about finitely many sentences to suitable probabilities over all sentences, and in particular least dogmatic or least biased ones. We conclude with a brief outlook on how the developed theory might be used and approximated in autonomous reasoning agents. Our theory is a step towards a globally consistent and empirically satisfactory unification of probability and logic.
  
  PubDate: 2013-03-20T03:07:19Z
Ultralarge lotteries: Analyzing the Lottery Paradox using non-standard analysis
- Abstract: Available online 15 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  A popular way to relate probabilistic information to binary rational beliefs is the Lockean Thesis, which is usually formalized in terms of thresholds. This approach seems far from satisfactory: the value of the thresholds is not well-specified and the Lottery Paradox shows that the model violates the Conjunction Principle. We argue that the Lottery Paradox is a symptom of a more fundamental and general problem, shared by all threshold-models that attempt to put an exact border on something that is intrinsically vague. We propose application of the language of relative analysis—a type of non-standard analysis—to formulate a new model for rational belief, called Stratified Belief. This contextualist model seems well-suited to deal with a concept of beliefs based on probabilities ‘sufficiently close to unity’ and satisfies a moderately weakened form of the Conjunction Principle. We also propose an adaptation of the model that is able to deal with beliefs that are less firm than ‘almost certainty’. The adapted version is also of interest for the epistemicist account of vagueness.
  
  PubDate: 2013-03-16T03:06:55Z
Representation of interlaced trilattices
- Abstract: Available online 14 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  Trilattices are algebraic structures introduced ten years ago into logic with the aim to provide a uniform framework for the notions of constructive truth and constructive falsity. In more recent years, trilattices have been used to introduce a number of many-valued systems that generalize the Belnap-Dunn logic of first-degree entailment, proposed as logics of how several computers connected together in a network should think in order to deal with incomplete and possibly contradictory information. The aim of the present work is to develop a first purely algebraic study of trilattices, focusing in particular on the problem of representing certain subclasses of trilattices as special products of bilattices. This approach allows to extend the known representation results for interlaced bilattices to the setting of trilattices and to reduce many algebraic problems concerning these new structures to the better-known framework of lattice theory.
  
  PubDate: 2013-03-16T03:06:55Z
A note on orthogonality of subspaces in Euclidean geometry
- Abstract: Available online 1 March 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  We show that Euclidean geometry in suitably high dimension can be expressed as a theory of orthogonality of subspaces with fixed dimensions and fixed dimension of their meet.
  
  PubDate: 2013-03-04T03:08:32Z
Two adaptive logics of norm-propositions
- Abstract: Available online 9 February 2013
  Publication year: 2013
  Source:Journal of Applied Logic
  
  We present two defeasible logics of norm-propositions (statements about norms) that (i) consistently allow for the possibility of normative gaps and normative conflicts, and (ii) map each premise set to a sufficiently rich consequence set. In order to meet (i), we define the logic LNP, a conflict- and gap-tolerant logic of norm-propositions capable of formalizing both normative conflicts and normative gaps within the object language. Next, we strengthen LNP within the adaptive logic framework for non-monotonic reasoning in order to meet (ii). This results in the adaptive logics LNP r and LNP m , which interpret a given set of premises in such a way that normative conflicts and normative gaps are avoided ‘whenever possible’. LNP r and LNP m are equipped with a preferential semantics and a dynamic proof theory.
  
  PubDate: 2013-02-12T01:35:09Z
Editorial Board
- Abstract: March 2013
  Publication year: 2013
  Source:Journal of Applied Logic, Volume 11, Issue 1
  
  PubDate: 2013-01-23T09:13:25Z
The Ackermann approach for modal logic, correspondence theory and second-order reduction
- Abstract: March 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 1
  
  The problem of eliminating second-order quantification over predicate symbols is in general undecidable. Since an application of second-order quantifier elimination is correspondence theory in modal logic, understanding when second-order quantifier elimination methods succeed is an important problem that sheds light on the kinds of axioms that are equivalent to first-order correspondence properties and can be used to obtain complete axiomatizations for modal logics. This paper introduces a substitution-rewrite approach based on Ackermannʼs Lemma to second-order quantifier elimination in modal logic. Compared to related approaches, the approach includes a number of enhancements: The quantified symbols that need to be eliminated can be flexibly specified. The inference rules are restricted by orderings compatible with the elimination order, which provides more control and reduces non-determinism in derivations thereby increasing the efficiency and success rate. The approach is equipped with a powerful notion of redundancy, allowing for the flexible definition of practical simplification and optimization techniques. We present correctness, termination and canonicity results, and consider two applications: (i) computing first-order frame correspondence properties for modal axioms and rules, and (ii) rewriting second-order modal problems to equivalent simpler forms. The approach allows us to define and characterize two new classes of formulae, which are elementary and canonical, and subsume the class of Sahlqvist formulae and the class of monadic inductive formulae.
  
  PubDate: 2012-12-18T09:16:16Z
Editorial Board
- Abstract: March 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 1
  
  PubDate: 2012-12-18T09:16:16Z
Special issue on Automated Specification and Verification of Web Systems
- Abstract: March 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 1
  
  PubDate: 2012-12-18T09:16:16Z
A calculus for orchestration of web services
- Abstract: March 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 1
  
  Service-oriented computing, an emerging paradigm for distributed computing based on the use of services, is calling for the development of tools and techniques to build safe and trustworthy systems, and to analyse their behaviour. Therefore, many researchers have proposed to use process calculi, a cornerstone of current foundational research on specification and analysis of concurrent, reactive, and distributed systems. In this paper, we follow this approach and introduce C WS, a process calculus expressly designed for specifying and combining service-oriented applications, while modelling their dynamic behaviour. We show that C WS can model all the phases of the life cycle of service-oriented applications, such as publication, discovery, negotiation, orchestration, deployment, reconfiguration and execution. We illustrate the specification style that C WS supports by means of a large case study from the automotive domain and a number of more specific examples drawn from it.
  
  PubDate: 2012-12-18T09:16:16Z
Translating regular expression matching into transducers
- Abstract: March 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 1
  
  Regular expression matching is an essential tool in string manipulating programs and plays crucial roles in scripting languages. We focus on regular expression matching based on the strategy of Perl and develop a translation from regular expression matching into transducers. The representation makes it possible to apply the theory of formal languages in static analysis and verification of string manipulating programs. We first formulate the semantics of regular expression matching as a nondeterministic parser by using the composition of the list and output monads. Then, we transform the nondeterministic parser into deterministic one by introducing lookahead. The deterministic parser is formulated with the option monad instead of the list monad and derived through equational reasoning involving monads. From the definition of the deterministic parser, we can easily construct transducers through transducers with regular lookahead. We have implemented the translation and conducted experiments on regular expressions found in several popular PHP programs.
  
  PubDate: 2012-12-18T09:16:16Z
Correlations of spaces of pencils
- Abstract: June 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 2
  
  The paper introduces an axiomatic system of a conjugacy in partial linear spaces, and provides its analytical characterization in spaces of pencils. A correlation of a space of pencils is defined and it is shown to correspond to a polarity of the underlying projective space, i.e. to a reflexive sesqui-linear form, or also to an involutory collineation, i.e. to an injective semi-linear map, in the self-dual case. A geometric characterization of segment subspaces in spaces of pencils is also provided.
  
  PubDate: 2012-12-18T09:16:16Z
Unity in nominal equational reasoning: The algebra of equality on nominal sets
- Abstract: June 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 2
  
  There are currently no fewer than four dedicated logics for equality reasoning over nominal sets: nominal algebra, nominal equational logic, nominal equational logic with equality only, and permissive-nominal algebra. In this survey and research paper we present these logics side-by-side in a common notation, survey their similarities and differences, discuss their proof- and model-theories, and discuss in detail what the implications of those differences are for mathematical reasoning in each of them.
  
  PubDate: 2012-12-18T09:16:16Z
Editorial Board
- Abstract: June 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 2
  
  PubDate: 2012-12-18T09:16:16Z
Reasoning about visibility
- Abstract: June 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 2
  
  We consider properties of sequences of spatial regions, as seen from a viewpoint. In particular, we concentrate on two types of regions: (1) general domains in which a region is any subset of the space, and (2) axis-parallel domains, where the regions are boxes in an N-dimensional space. We introduce binary relations allowing to express properties of these sequences and present two approaches to process them. First, we show that constraints on these relations can be solved in polynomial time for general domain and that the same problem is NP-complete in the axis-parallel case. Second, we introduce a modal logic on these relations, called Visibility Logic, and show that model-checking on a finite sequence of regions can be done in polynomial time (both in the general and axis-parallel cases). Finally, we present applications to image processing and firewall filtering.
  
  PubDate: 2012-12-18T09:16:16Z
An optimal construction of Hanf sentences
- Abstract: June 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 2
  
  We give a new construction of formulas in Hanf normal form that are equivalent to first-order formulas over structures of bounded degree. This is the first algorithm whose running time is shown to be elementary. The triply exponential upper bound is complemented by a matching lower bound.
  
  PubDate: 2012-12-18T09:16:16Z
Future determination of entities in Talmudic public announcement logic
- Abstract: Available online 12 June 2012
  Publication year: 2012
  Source:Journal of Applied Logic
  
  Ordinary dynamic action logics deal with states and actions upon states. The actions can be deterministic or non-deterministic, but it is always assumed that the possible results of the actions are clear cut. Talmudic logic deals with actions (usually legally meaningful actions which can change the legal status of an entity) which depend on the future and therefore may be not clear cut at the present and need future clarifications. The clarification is modelled by public announcement which comes at a later time after the action has taken place. The model is further complicated by the need to know what is the status of formulas at a time before the results of the action is clarified, as we do not know at which state we are in. Talmudic logic treats such states much like the quantum superposition of states and when clarification is available we get a collapse onto a pure state. The Talmudic lack of clarity of actions arises from applying an action to entities defined using the future, like the statement of a dying man on his death bed: Let the man who will win the jackpot in the lottery next week be the sole heir in my will now We need to wait a week for the situation to clarify. There is also the problem of legal backwards causality, as this man, if indeed he exists, unaware of his possible good fortune, may have himself meanwhile donated all his property to a charity. Does his donation include this unknown inheritance' This paper will offer a model and a logic which can represent faithfully the Talmudic reasoning in these matters. We shall also see that we get new types of public announcement logics and (quantum-like) action logics. Ordinary public announcement logic deletes possible worlds after an announcements. Talmudic public announcement logic deletes accessibility links after an announcement. Technically these two approaches are similar but not equivalent.
  
  PubDate: 2012-12-18T09:16:16Z
Deciding the word problem in pure double Boolean algebras
- Abstract: September 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 3
  
  Pure double Boolean algebras have attracted interest both for their theoretical merits and for their practical relevance. The aim of this article is to investigate the decidability and the complexity of the word problem in pure double Boolean algebras.
  
  PubDate: 2012-12-18T09:16:16Z
Denotation of contextual modal type theory (CMTT): Syntax and meta-programming
- Abstract: Available online 15 July 2012
  Publication year: 2012
  Source:Journal of Applied Logic
  
  The modal logic S4 can be used via a Curry–Howard style correspondence to obtain a λ-calculus. Modal (boxed) types are intuitively interpreted as ‘closed syntax of the calculus’. This λ-calculus is called modal type theory—this is the basic case of a more general contextual modal type theory, or CMTT. CMTT has never been given a denotational semantics in which modal types are given denotation as closed syntax. We show how this can indeed be done, with a twist. We also use the denotation to prove some properties of the system.
  
  PubDate: 2012-12-18T09:16:16Z
Deductive temporal reasoning with constraints
- Abstract: Available online 14 July 2012
  Publication year: 2012
  Source:Journal of Applied Logic
  
  When modelling realistic systems, physical constraints on the resources available are often required. For example, we might say that at most N processes can access a particular resource at any moment, exactly M participants are needed for an agreement, or an agent can be in exactly one mode at any moment. Such situations are concisely modelled where literals are constrained such that at most N, or exactly M, can hold at any moment in time. In this paper we consider a logic which is a combination of standard propositional linear time temporal logic with cardinality constraints restricting the numbers of literals that can be satisfied at any moment in time. We present the logic and show how to represent a number of case studies using this logic. We propose a tableau-like algorithm for checking the satisfiability of formulae in this logic, provide details of a prototype implementation and present experimental results using the prover.
  
  PubDate: 2012-12-18T09:16:16Z
Opacity and the double life of singular propositions
- Abstract: September 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 3
  
  In this paper I analyze David Kaplanʼs essay “Opacity”. In “Opacity” Kaplan attempts to dismiss Quineʼs concerns about quantification across intensional (modal and intentional) operators. I argue that Kaplan succeeds in showing that quantification across intensional operators is logically coherent and that quantified modal logic is strictly speaking not committed to essentialism. However, I also argue that this is not in and of itself sufficient to support Kaplanʼs more ambitious attempt to move beyond purely logical results and provide unified, uncontroversial interpretations of both “believes” and “necessarily”. In the paper I raise several questions about the subject matter of logic and the role of semantics, with special focus on singular propositions.
  
  PubDate: 2012-12-18T09:16:16Z
Quine on intensional entities: Modality and quantification, truth and satisfaction
- Abstract: September 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 3
  
  In this paper, I reconstruct Quineʼs arguments against quantified modal logic, from the early 1940ʼs to the early 1960ʼs. Quineʼs concerns were not technical. Quine was looking for a coherent interpretation of quantified-in English modal sentences. I argue that Quineʼs main thesis is that the intended objectual interpretation of the quantifiers is incompatible with any semantic reading of the modal operators, for example as expressing analytic necessity, unless the entities in the domain of quantification are intensions, i.e. definitional entities. The difficulty is that it makes no sense to say of an ordinary object that it bears a property necessarily or contingently when the necessity or contingency in question is analytic. However, starting in 1960, Quine claims that quantified-in modal sentences can be coherently interpreted only as essentialist predications. When we say about an object that it necessarily Fʼs, we can only coherently mean that it essentially Fʼs. In the paper, I argue that adequately qualified the thesis is plausible. Two important qualifications are needed. The first is the assumption that satisfaction is an irreducibly predicative notion, making any explication of satisfaction in terms of truth inadequate. The second is the ontological rejection of purely semantic, i.e. merely definitional, entities. With these qualifications in place, Quineʼs rejection of the combination of objectual quantifiers and semantic modalities can be upheld. In this way, we vindicate a qualified version of Quineʼs conjecture that quantified modal logic is committed to essentialism.
  
  PubDate: 2012-12-18T09:16:16Z
Editorial Board
- Abstract: September 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 3
  
  PubDate: 2012-12-18T09:16:16Z
Temporal alethic–deontic logic and semantic tableaux
- Abstract: September 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 3
  
  The purpose of this paper is to describe a set of temporal alethic–deontic systems, i.e. systems that include temporal, alethic and deontic operators. All in all we will consider 2,147,483,648 systems. All systems are described both semantically and proof theoretically. We use a kind of possible world semantics, inspired by the so-called T×W semantics, to characterize our systems semantically and semantic tableaux to characterize them proof theoretically. We also show that all systems are sound and complete with respect to their semantics.
  
  PubDate: 2012-12-18T09:16:16Z
A logic of non-monotonic interactions
- Abstract: Available online 28 September 2012
  Publication year: 2012
  Source:Journal of Applied Logic
  
  In this paper, which is part of the Zsyntax project outlined in Boniolo et al. (2010) [2], we provide a proof-theoretical setting for the study of context-sensitive interactions by means of a non-monotonic conjunction operator. The resulting system is a non-associative variant of MLL pol (the multiplicative polarised fragment of Linear Logic) in which the monotonicity of interactions, depending on the context, is governed by specific devices called control sets. Following the spirit of Linear Logic, the ordinary sequent calculus presentation is also framed into a theory of proof-nets and the set of sequential proofs is shown to be sound and complete with respect to the class of corresponding proof-nets. Some possible biochemical applications are also discussed.
  
  PubDate: 2012-12-18T09:16:16Z
Reactive Kripke models and contrary to duty obligations. Part A: Semantics
- Abstract: Available online 15 September 2012
  Publication year: 2012
  Source:Journal of Applied Logic
  
  This paper introduces a new method for modelling contrary to duty obligations (CTD). Given a contrary to duty obligation structure CTDs presented in English, there is the problem of offering a logical system in which it can be coherently formalised. There are several formal systems in the literature attempting to do so, such as SDL (Standard Deontic Logic), various dyadic operators and other kinds of formalised normative systems. The difficulties encountered by such systems is that they end up with counter intuitive results for some CTD linguistic structures, referred to as paradoxes (for the offered formalising logic). We use reactive Kripke models as the semantics and a reactive extension of SDL, with one additional reactive modality as syntax for such CTD. Reactive Kripke models change their accessibility relation as we move from node to node during the semantic evaluation process. This change is made to correspond to the change implicit in the intuitive meaning of the contrary to duty obligations. The reactive Kripke semantics is stronger semantics than ordinary Kripke models and therefore allows for more fine tuning of our modelling process.
  
  PubDate: 2012-12-18T09:16:16Z
The countable versus uncountable branching recurrences in computability logic
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  This paper introduces a new simplified version of the countable branching recurrence of Computability Logic, proves its equivalence to the old one, and shows that the basic logic induced by (i.e., the one in the signature { ¬ , ∧ , ∨ , , } ) is a proper superset of the basic logic induced by the uncountable branching recurrence (i.e., the one in the signature { ¬ , ∧ , ∨ , , } ). A further result of this paper is showing that is strictly weaker than in the sense that F logically implies F but not vice versa.
  
  PubDate: 2012-12-18T09:16:16Z
A planner agent that tries its best in presence of nondeterminism
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  In many nondeterministic planning domains, an agent whose goal is to achieve φ may not succeed in finding a policy that can guarantee that all paths from the initial state lead to a final state where φ holds (strong solution). Nevertheless, if the agent is trying its best to achieve φ, it cannot give up. Instead, it may be inclined to accept weaker guarantees, such as having a path leading to φ from any intermediate state reached by the policy (strong-cyclic solution), or even less, such as having at least one path leading to φ from the initial state (weak solution). But the agent should choose among such different options based on their availability in each situation. Although the specification of this type of goal has been addressed before, in this paper we show how a planner based on the branching time temporal logic α-ctl can be used to plan for intuitive and useful goals of the form “try your best to achieve φ”.
  
  PubDate: 2012-12-18T09:16:16Z
Automata for the verification of monadic second-order graph properties
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  The model-checking problem for monadic second-order logic on graphs is fixed-parameter tractable with respect to tree-width and clique-width. The proof constructs finite automata from monadic second-order sentences. These automata recognize the terms over fixed finite signatures that define graphs satisfying the given sentences. However, this construction produces automata of hyper-exponential sizes, and is thus impossible to use in practice in many cases. To overcome this difficulty, we propose to specify the transitions of automata by programs instead of tables. Such automata are called fly-automata. By using them, we can check certain monadic second-order graph properties with limited quantifier alternation depth, that are nevertheless interesting for Graph Theory. We give explicit constructions of automata relative to graphs of bounded clique-width, and we report on experiments.
  
  PubDate: 2012-12-18T09:16:16Z
Improving the semantics of the Software Cost Reduction method
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  Although the Software Cost Reduction (SCR) method has been successfully used in many projects and organizations to specify software requirements, surprisingly, its semantics is not well defined. The symbols used in this method are ambiguous, especially those that serve to denote SCR events. The aim of this work is to address this ambiguity and improve the SCR semantics by enabling events in first-order logic via two symbols pred and succ. This slight extension of first-order logic allows us to increase the readability of the SCR tables, eliminate their ambiguous semantics, facilitate the verification and validation process, and improve the toolset supporting the SCR method, just to name a few. Moreover, our extension is simple and avoids the complexity of temporal logic.
  
  PubDate: 2012-12-18T09:16:16Z
A domain specific language for describing diverse systems of dialogue
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  This paper introduces the Dialogue Game Description Language (DGDL), a domain specific language for describing dialectical games. Communication is an important topic within agent research and is a fundamental factor in the development of robust and efficient multiagent systems. Similarly, argumentation has been recognised as a key component of an agentʼs ability to make decisions using complex, dynamic, uncertain, and incomplete knowledge. Dialectical games, a type of multi-player argumentative dialogue game, provide a mechanism for communication which incorporates argumentative behaviours. However there are very few tools for working with these games and little agreement over how they should be described, shared, and reused. The DGDL provides a grammar for determining whether a game description is syntactically correct and thus provides a foundation for new tools to support the future development and wider exploitation of dialectical games.
  
  PubDate: 2012-12-18T09:16:16Z
Cut elimination for a logic with induction and co-induction
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles are based on a proof-theoretic (rather than set-theoretic) notion of definition (Hallnäs, 1991 [18], Eriksson, 1991 [11], Schroeder-Heister, 1993 [38], McDowell and Miller, 2000 [22]). Definitions are akin to logic programs, where the left and right rules for defined atoms allow one to view theories as “closed” or defining fixed points. The use of definitions and free equality makes it possible to reason intensionally about syntax. We add in a consistent way rules for pre- and post-fixed points, thus allowing the user to reason inductively and co-inductively about properties of computational system making full use of higher-order abstract syntax. Consistency is guaranteed via cut-elimination, where we give a direct cut-elimination procedure in the presence of general inductive and co-inductive definitions via the parametric reducibility technique.
  
  PubDate: 2012-12-18T09:16:16Z
Combining genetic algorithms and the finite element method to improve steel industrial processes
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  Most of the times the optimal control of steel industrial processes is a very complicated task because of the elevated number of parameters to adjust. For that reason, in steel plants, engineers must estimate the best values of the operational parameters of processes, and sometimes, it is also necessary to obtain the appropriate model for steel material behaviour. This article deals with three successful experiences gained from genetic algorithms and the finite element method in order to solve engineering optimisation problems. On one hand, a fully automated method for determining the best material behaviour laws is described, and on the other hand we present a common methodology to find the most appropriate settings for two cases of improvement in steel industrial processes. The study of the three reported cases allowed us to show the reliability and effectiveness of combining both techniques.
  
  PubDate: 2012-12-18T09:16:16Z
Automatic detection of bunches of grapes in natural environment from color images
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  Despite the benefits of precision agriculture and precision viticulture production systems, its rate of adoption in the Portuguese Douro Demarcated Region remains low. We believe that one way to raise it is to address challenging real-world problems whose solution offers a clear benefit to the viticulturist. For example, one of the most demanding tasks in wine making is harvesting. Even for humans, the environment makes grape detection difficult, especially when the grapes and leaves have a similar color, which is generally the case for white grapes. In this paper, we propose a system for the detection and location, in the natural environment, of bunches of grapes in color images. This system is able to distinguish between white and red grapes, and at the same time, it calculates the location of the bunch stem. The system achieved 97% and 91% correct classifications for red and white grapes, respectively.
  
  PubDate: 2012-12-18T09:16:16Z
Pitting corrosion behaviour of austenitic stainless steel using artificial intelligence techniques
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  Different artificial intelligent tools have been used to model pitting corrosion behaviour of EN 1.4404 austenitic stainless steel. Samples from this material have been subjected to polarization tests in different chloride solutions using different precursor salts: NaCl and MgCl2. The aim of this work is to compare the results obtained from the different classification models using both solutions studying the influence of them. Furthermore, in order to determine pitting potential values ( E pit ), different environmental conditions have been tested varying chloride ion concentration, pH value and temperature. The techniques used try to find the relation between the environmental parameters studied and the status pitting corrosion of this alloy. Several classification techniques have been used: Classification Trees (CT), Discriminant Analysis (DA), K-Nearest-Neighbours (K-NN), Back-Propagation Neural Networks (BPNN) and Support Vector Machine (SVM). The results obtained show the good correlation between experimental and predicted data for all the cases studied demonstrating the utility of artificial intelligence for modelling pitting corrosion problem.
  
  PubDate: 2012-12-18T09:16:16Z
Selected papers from the 6th International Conference on Soft Computing Models in Industrial and Environmental Applications
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  PubDate: 2012-12-18T09:16:16Z
Breast cancer MRI diagnosis approach using support vector machine and pulse coupled neural networks
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  This article introduces a hybrid approach that combines the advantages of fuzzy sets, pulse coupled neural networks (PCNNs), and support vector machine, in conjunction with wavelet-based feature extraction. An application of breast cancer MRI imaging has been chosen and hybridization approach has been applied to see their ability and accuracy to classify the breast cancer images into two outcomes: normal or non-normal. The introduced approach starts with an algorithm based on type-II fuzzy sets to enhance the contrast of the input images. This is followed by performing PCNN-based segmentation algorithm in order to identify the region of interest and to detect the boundary of the breast pattern. Then, wavelet-based features are extracted and normalized. Finally, a support vector machine classifier was employed to evaluate the ability of the lesion descriptors for discrimination of different regions of interest to determine whether they represent cancer or not. To evaluate the performance of presented approach, we present tests on different breast MRI images. The experimental results obtained, show that the overall accuracy offered by the employed machine learning techniques is high compared with other machine learning techniques including decision trees, rough sets, neural networks, and fuzzy artmap.
  
  PubDate: 2012-12-18T09:16:16Z
An intelligent task analysis approach for special education based on MIRA
- Abstract: Available online 14 December 2012
  Publication year: 2012
  Source:Journal of Applied Logic
  
  This paper describes a novel approach for generating a logical sequence of tasks in the task analysis process of special education. This approach is based on the formalism MIRA (Mīmāṁsā Inspired Representation of Actions), which has the feature of expressing an action as reason, instruction and goal. MIRA also prescribes a set of deduction rules, which helps in the reasoning process of actions. These features are incorporated in this approach and a software tool, namely MIRATaskGen is designed, which facilitates the task analysis process of special education. The software receives various action related inputs along with the start and finish stages and generates a sequence of tasks from the start to finish. This tool also informs the user, whether the desired goal can be achieved. If the desired goal cannot be achieved, then the sequence of actions from the start to a point of discontinuity is detected.
  
  PubDate: 2012-12-18T09:16:16Z
LEO-II and Satallax on the Sledgehammer test bench
- Abstract: Available online 13 December 2012
  Publication year: 2012
  Source:Journal of Applied Logic
  
  Sledgehammer is a tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEO-II and Satallax, the two most prominent higher-order ATPs, improving its performance on higher-order problems. To explore their usefulness, these ATPs are measured against first-order ATPs and built-in Isabelle tactics on a variety of benchmarks from Isabelle and the TPTP library. Sledgehammer provides an ideal test bench for individual features of LEO-II and Satallax, revealing areas for improvements.
  
  PubDate: 2012-12-18T09:16:16Z
Editorial Board
- Abstract: December 2012
  Publication year: 2012
  Source:Journal of Applied Logic, Volume 10, Issue 4
  
  PubDate: 2012-12-18T09:16:16Z