Functional un|unparsing

Danvy??s functional unparsing problem (Danvy in J. Funct. Program. 8(6), 621?C625, 1998) is to implement a type-safe ??printf?? function, which converts a sequence of heterogeneous arguments to a string according to a given format. The dual problem is to implement a type-safe ??scanf?? function, which extracts a sequence of heterogeneous arguments from a string by interpreting (Friedman and Wand in LFP, pp. 348?C355, 1984 and in Essentials of Programming Languages, MIT Press, 2008) the same format as an equally heterogeneous sequence of patterns that binds zero or more variables. We derive multiple solutions to both problems (Wand in J. ACM 27(1), 164?C180, 1980) from their formal specifications (Wand in Theor. Comput. Sci. 20(1), 3?C32, 1982). On one hand, our solutions show how the Hindley-Milner type system, unextended, permits accessing heterogeneous sequences with the static assurance of type safety. On the other hand, our solutions demonstrate the use of control operators (Felleisen et al. in Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pp. 52?C62, ACM Press, New York, 1988; Wand in POPL 85: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, vol. 16, ACM Press, New York, 1985; Meyer and Wand in Logics of Programs, Lecture Notes in Computer Science, vol. 193, pp. 219?C224, Springer, Berlin, 1985) to communicate with formats as coroutines (Wand in Proceedings of the 1980 ACM Conference on Lisp and Functional Programming, vol. 12, pp. 285?C299, ACM Press, New York, 1980 and Haynes et al. in LFP, pp. 293?C298, 1984).     

Wherein is Human Cognition Systematic?

The ??systematicity argument?? has been used to argue for a classical cognitive architecture (Fodor in The Language of Thought. Harvester Press, London, 1975, Why there still has to be a language of thought? In Psychosemantics, appendix. MIT Press, Cambridge, pp 135?C154, 1987; Fodor and Pylyshyn in Cognition 28:3?C71, 1988; Aizawa in The systematicity arguments. Kluwer Academic Press, Dordrecht, 2003). From the premises that cognition is systematic and that the best/only explanation of systematicity is compositional structure, it concludes that cognition is to be explained in terms of symbols (in a language of thought) and formal rules. The debate, with connectionism, has mostly centered on the second premise-whether an explanation of systematicity requires compositional structure, which neural networks do not to exhibit (for example, Hadley and Hayward, in Minds and Machines, 7:1?C37). In this paper, I will take issue with the first premise. Several arguments will be deployed that show that cognition is not systematic in general; that, in fact, systematicity seems to be related to language. I will argue that it is just verbal minds that are systematic, and they are so because of the structuring role of language in cognition. A dual-process theory of cognition will be defended as the best explanation of the facts.     

A logic of argumentation for specification and verification of abstract argumentation frameworks

In this paper, we propose a logic of argumentation for the specification and verification (LA4SV) of requirements on Dung??s abstract argumentation frameworks. We distinguish three kinds of decision problems for argumentation verification, called extension verification, framework verification, and specification verification respectively. For example, given a political requirement like ??if the argument to increase taxes is accepted, then the argument to increase services must be accepted too,?? we can either verify an extension of acceptable arguments, or all extensions of an argumentation framework, or all extensions of all argumentation frameworks satisfying a framework specification. We introduce the logic of argumentation verification to specify such requirements, and we represent the three verification problems of argumentation as model checking and theorem proving properties of the logic. Moreover, we recast the logic of argumentation verification in a modal framework, in order to express multiple extensions, and properties like transitivity and reflexivity of the attack relation. Finally, we introduce a logic of meta-argumentation where abstract argumentation is used to reason about abstract argumentation itself. We define the logic of meta-argumentation using the fibring methodology in such a way to represent attack relations not only among arguments but also among attacks. We show how to use this logic to verify the requirements of argumentation frameworks where higher-order attacks are allowed [A preliminary version of the logic of argumentation compliance was called the logic of abstract argumentation?(2005).]     

Hierarchical object-driven action rules

In this work, we present the hierarchical object-driven action rules; a hybrid action rule extraction approach that combines key elements from both the classical action rule mining approach, first proposed by Ra? and Wieczorkowska (2000), and the more recent object-driven action rule extraction approach proposed by Hajja et al. (2012, 2013), to extract action rules from object-driven information systems. Action rules, as defined in Ra? and Wieczorkowska (2000), are actionable tasks that describe possible transitions of instances from one state to another with respect to a distinguished attribute, called the decision attribute. Recently, a new specialized case of action rules, namely object-driven action rules, has been introduced by Hajja et al. (2012, 2013). Object-driven action rules are action rules that are extracted from information systems with temporal and object-based nature. By object-driven information systems, we mean systems that contain multiple observations for each object, in which objects are determined by an attribute that assumingly defines some unique distribution; and by temporally-based information systems, we refer to systems in which each instance is attached to a timestamp that, by definition, must have an intrinsic meaning for each corresponding instance. Though the notion of object-driven and temporal-based action rules had its own successes, some argue that the essence of object-driven assumptions, which is in big part the reason for its effectiveness, are imposing few limitations as well. Object-driven approaches treat entire systems as multi-subsystems for which action rules are extracted from; as a result, more accurate and specific action rules are extracted. However, by doing so, our diverseness of the extracted action rules are much less apparent, compared to the outcome when applying the classical action rule extraction approach, which treats information systems as a whole. For that reason, we propose a hybrid approach which builds a hierarchy of clusters of subsystems; a novel way of clustering through treatments responses similarities is introduced.     

Better and Simpler Approximation Algorithms for?the?Stable Marriage Problem

We first consider the problem of finding a maximum size stable matching if incomplete lists and ties are both allowed, but ties are on one side only. For this problem we give a simple, linear time 3/2-approximation algorithm, improving on the best known approximation factor 5/3 of Irving and Manlove (J. Comb. Optim., doi:10.1007/s10878-007-9133-x, 2007). Next, we show how this extends to the Hospitals/Residents problem with the same ratio if the residents have strict orders. We also give a simple linear time algorithm for the general problem with approximation factor 5/3, improving the best known 15/8-approximation algorithm of Iwama, Miyazaki and Yamauchi (SODA ??07: Proceedings of the Eighteenth Annual ACM-SIAM Symposium on Discrete Algorithms, pp.?288?C297, 2007). For the cases considered in this paper it is NP-hard to approximate within a factor of 21/19 by the result of Halldórsson et?al. (ACM Transactions on Algorithms 3(3):30, 2007). Our algorithms not only give better approximation ratios than the cited ones, but are much simpler and run significantly faster. Also we may drop a restriction used in (J. Comb. Optim., doi:10.1007/s10878-007-9133-x, 2007) and the analysis is substantially more moderate. Preliminary versions of this paper appeared in (Király, Egres Technical Report TR-2008-04, www.cs.elte.hu/egres/, 2008; Király in Proceedings of MATCH-UP 2008: Matching Under Preferences??Algorithms and Complexity, Satellite Workshop of ICALP, July 6, 2008, Reykjavík, Iceland, pp.?36?C45, 2008; Király in ESA 2008, Lecture Notes in Computer Science, vol.?5193, pp.?623?C634, 2008). For the related results obtained thenceforth see Sect.?5.     

Expected Optimal Feedback with Time-Varying Parameters

In this paper we derive the closed loop form of the Expected Optimal Feedback rule, sometimes called passive learning stochastic control, with time varying parameters. As such this paper extends the work of Kendrick (Stochastic control for economic models, 1981; Stochastic control for economic models, 2002, Chap. 6) where parameters are assumed to vary randomly around a known constant mean. Furthermore, we show that the cautionary myopic rule in Beck and Wieland (J Econ Dyn Control 26:1359–1377, 2002) model, a test bed for comparing various stochastic optimizations approaches, can be cast into this framework and can be treated as a special case of this solution.     

Modelling defeasible and prioritized support in bipolar argumentation

Cayrol and Lagasquie-Schiex introduce bipolar argumentation frameworks by introducing a second relation on the arguments for representing the support among them. The main drawback of their approach is that they cannot encode defeasible support, for instance they cannot model an attack towards a support relation. In this paper, we introduce a way to model defeasible support in bipolar argumentation frameworks. We use the methodology of meta-argumentation in which Dung??s theory is used to reason about itself. Dung??s well-known admissibility semantics can be used on this meta-argumentation framework to compute the acceptable arguments, and all properties of Dung??s classical theory are preserved. Moreover, we show how different contexts can lead to the alternative strengthening of the support relation over the attack relation, and converse. Finally, we present two applications of our methodology for modeling support, the case of arguments provided with an internal structure and the case of abstract dialectical frameworks.     

Confirmation of Lagrange hypothesis for twisted elastic rod

The history of structural optimization as an exact science begins possibly with the celebrated Lagrange problem: to find a curve which by its revolution about an axis in its plane determines the rod of greatest efficiency (Lagrange 1868). The Lagrange hypothesis, that the optimal rod possesses the constant cross-section was abandoned for Euler buckling problem (Tadjbakhsh and Keller, J Appl Mech 29:159?C164, 1962). In this Article the Lagrange hypothesis is proved to be valid for Greenhill??s problem of torque buckling. The corresponding isoperimetric inequality is affirmed.     

Incentive-compatible interdomain routing

The routing of traffic between Internet domains, or Autonomous Systems (ASes), a task known as interdomain routing, is currently handled by the Border Gateway Protocol (BGP, Rekhter and Li in RFC 4271 of the Internet Engineering Task Force, 2006). Using BGP, ASes can apply semantically rich routing policies to choose interdomain routes in a distributed fashion. This expressiveness in routing-policy choice supports domains?? autonomy in network operations and in business decisions, but it comes at a price: The interaction of locally defined routing policies can lead to unexpected global anomalies, including route oscillations or overall protocol divergence (see, e.g., Varadhan et?al. in Comput Networks 32(1):1?C16, 2000). Networking researchers have addressed this problem by devising constraints on policies that guarantee BGP convergence without unduly limiting expressiveness and autonomy (see, e.g., Gao and Rexford in IEEE/ACM Trans Network 9(6):681?C692, 2001; Griffin et?al. in Proceedings of 9th ACM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM??03), pp. 61?C72. ACM Press, New York, 2003). In addition to taking this engineering or ??protocol- design?? approach, researchers have approached interdomain routing from an economic or ??mechanism-design?? point of view. It is known that lowest-cost-path (LCP) routing can be implemented in an incentive-compatible, BGP-compatible manner (Feigenbaum et?al. in Distribut. Comput 18(1):61?C72, 2005; Shneidman and Parkes in Proceedings of 23rd ACM Symposium on Principles of Distributed Computing (PODC??04), pp. 88?C97. ACM Press, New York, 2004) but that several other natural classes of policies cannot (Feigenbaum et?al. in Theor Comput Sci 378(2):175?C189, 2007; Feigenbaum et?al. in Distribut Comput 18(4):293?C305, 2006). In this paper, we present the first example of a class of interdomain-routing policies that is more general than LCP routing and for which BGP itself is both incentive-compatible and guaranteed to converge. We also present several steps toward a general theory of incentive-compatible, BGP-compatible interdomain routing.     

How to Build a Robot that is Conscious and Feels

Following arguments put forward in my book (Why red doesn??t sound like a bell: understanding the feel of consciousness. Oxford University Press, New York, USA, 2011), this article takes a pragmatic, scientist??s point of view about the concepts of consciousness and ??feel??, pinning down what people generally mean when they talk about these concepts, and then investigating to what extent these capacities could be implemented in non-biological machines. Although the question of ??feel??, or ??phenomenal consciousness?? as it is called by some philosophers, is generally considered to be the ??hard?? problem of consciousness, the article shows that by taking a ??sensorimotor?? approach, the difficulties can be overcome. What remains to account for are the notions of so-called ??access consciousness?? and the self. I claim that though they are undoubtedly very difficult, these are not logically impossible to implement in robots.     

t-DeLP: an argumentation-based Temporal Defeasible Logic Programming framework

The aim of this paper is to propose an argumentation-based defeasible logic, called t-DeLP, that focuses on forward temporal reasoning for causal inference. We extend the language of the DeLP logical framework by associating temporal parameters to literals. A temporal logic program is a set of basic temporal facts and (strict or defeasible) durative rules. Facts and rules combine into durative arguments representing temporal processes. As usual, a dialectical procedure determines which arguments are undefeated, and hence which literals are warranted, or defeasibly follow from the program. t-DeLP, though, slightly differs from DeLP in order to accommodate temporal aspects, like the persistence of facts. The output of a t-DeLP program is a set of warranted literals, which is first shown to be non-contradictory and be closed under sub-arguments. This basic framework is then modified to deal with programs whose strict rules encode mutex constraints. The resulting framework is shown to satisfy stronger logical properties like indirect consistency and closure.     

The loophole of the improved secure quantum sealed-bid auction with post-confirmation and solution

In the literature He et?al. (Quantum Inf Process, 2011) performed the cryptanalysis about the protocol of secure quantum auction with post-confirmation, and proposed the melioration algorithm in order to defeat the collusion among some malicious bidders in Zhao et?al.??s protocol (Zhao et?al. in Opt Commun 283:3194, 2010). But unfortunately, this protocol can??t defeat the collusion among some malicious bidders either. In this paper, we will analyze the security of He et?al.??s protocol and point out the potential loophole. Furthermore, we propose an improved protocol which can defeat the collusion among malicious bidders effectively.     

A Complete Superposition Calculus for Primal Grammars

The superposition calculus (Bachmair and Ganzinger, J. Log Comput. 3(4), 217–247, 1994; Nieuwenhuis and Rubio 1994) is the state-of-the-art inference system used in saturation-based theorem proving for first-order logic with equality.We present an extension of this calculus that permits us to reason on formulae built on primal grammars (Hermann and Galbavý, Theor. Comput. Sci. 176(1–2), 111–158, 1997) a schematization language that has been devised to denote infinite sequences of structurally similar terms, defined by primitive recursion. We prove that the calculus is sound and refutationally complete.     

Cross-categorization of legal concepts across boundaries of legal systems: in consideration of inferential links

This work contrasts Giovanni Sartor’s view of inferential semantics of legal concepts (Sartor in Artif Intell Law 17:217–251, 2009) with a probabilistic model of theory formation (Kemp et al. in Cognition 114:165–196, 2010). The work further explores possibilities of implementing Kemp’s probabilistic model of theory formation in the context of mapping legal concepts between two individual legal systems. For implementing the legal concept mapping, we propose a cross-categorization approach that combines three mathematical models: the Bayesian Model of Generalization (BMG; Tenenbaum and Griffiths in Behav Brain Sci 4:629–640, 2001), the probabilistic model of theory formation, i.e., the Infinite Relational Model (IRM) first introduced by Kemp et al. (The twenty-first national conference on artificial intelligence, 2006, Cognition 114:165–196, 2010) and its extended model, i.e., the normal-IRM (n-IRM) proposed by Herlau et al. (IEEE International Workshop on Machine Learning for Signal Processing, 2012). We apply our cross-categorization approach to datasets where legal concepts related to educational systems are respectively defined by the Japanese- and the Danish authorities according to the International Standard Classification of Education. The main contribution of this work is the proposal of a conceptual framework of the cross-categorization approach that, inspired by Sartor (Artif Intell Law 17:217–251, 2009), attempts to explain reasoner’s inferential mechanisms.     

Quantity-based buffer-constrained two-machine flowshop problem: active and passive prefetch models for multimedia applications

Conventional studies on buffer-constrained flowshop scheduling problems have considered applications with a limitation on the number of jobs that are allowed in the intermediate storage buffer before flowing to the next machine. The study in Lin et al. (Comput. Oper. Res. 36(4):1158?C1175, 2008a) considered a two-machine flowshop problem with ??processing time-dependent?? buffer constraints for multimedia applications. A???passive?? prefetch model (the PP-problem), in which the download process is suspended unless the buffer is sufficient for keeping an incoming media object, was applied in Lin et al. (Comput. Oper. Res. 36(4):1158?C1175, 2008a). This study further considers an ??active?? prefetch model (the AP-problem) that exploits the unoccupied buffer space by advancing the download of the incoming object by a computed maximal duration that possibly does not cause a buffer overflow. We obtain new complexity results for both problems. This study also proposes a new lower bound which improves the branch and bound algorithm presented in Lin et al. (Comput. Oper. Res. 36(4):1158?C1175, 2008a). For the PP-problem, compared to the lower bounds developed in Lin et al. (Comput. Oper. Res. 36(4):1158?C1175, 2008a), on average, the results of the simulation experiments show that the proposed new lower bound cuts about 38% of the nodes and 32% of the execution time for searching the optimal solutions.     

A Note on Intensionalization

Building on Ben-Avi and Winter’s (2007) work, this paper provides a general “intensionalization” procedure that turns an extensional semantics for a language into an intensionalized one that is capable of accommodating “truly intensional” lexical items without changing the compositional semantic rules. We prove some formal properties of this procedure and clarify its relation to the procedure implicit in Montague’s (1973) PTQ.     

A Logic for Reasoning About Knowledge of Unawareness

In the most popular logics combining knowledge and awareness, it is not possible to express statements about knowledge of unawareness such as “Ann knows that Bill is aware of something Ann is not aware of”—without using a stronger statement such as “Ann knows that Bill is aware of \(p\) and Ann is not aware of \(p\) ”, for some particular \(p\) . In Halpern and Rêgo (Proceedings of KR 2006; Games Econ Behav 67(2):503–525, 2009b) Halpern and Rêgo introduced a logic in which such statements about knowledge of unawareness can be expressed. The logic extends the traditional framework with quantification over formulae, and is thus very expressive. As a consequence, it is not decidable. In this paper we introduce a decidable logic which can be used to reason about certain types of unawareness. Our logic extends the traditional framework with an operator expressing full awareness, i.e., the fact that an agent is aware of everything, and another operator expressing relative awareness, the fact that one agent is aware of everything another agent is aware of. The logic is less expressive than Halpern’s and Rêgo’s logic. It is, however, expressive enough to express all of the motivating examples in Halpern and Rêgo (Proceedings of KR 2006; Games Econ Behav 67(2):503–525, 2009b). In addition to proving that the logic is decidable and that its satisfiability problem is PSPACE-complete, we present an axiomatisation which we show is sound and complete.     

Fermat’s last theorem and chaoticity

Proving that a dynamical system is chaotic is a central problem in chaos theory (Hirsch in Chaos, fractals and dynamics, 1985]. In this note we apply the computational method developed in (Calude and Calude in Complex Syst 18:267?C285, 2009; Calude and Calude in Complex Syst 18:387?C401, 2010; Calude et al in J Multi Valued Log Soft Comput 12:285?C307, 2006) to show that Fermat??s last theorem is in the lowest complexity class ${{\mathfrak C}_{U,1}}$ . Using this result we prove the existence of a two-dimensional Hamiltonian system for which the proof that the system has a Smale horseshoe is in the class ${{\mathfrak C}_{U,1}}$ , i.e. it is not too complex.     

Multi-Attacker Protocol Validation

Security protocols have been analysed focusing on a variety of properties to withstand the Dolev-Yao attacker. The Multi-Attacker treat model allows each protocol participant to behave maliciously intercepting and forging messages. Each principal may then behave as a Dolev-Yao attacker while neither colluding nor sharing knowledge with anyone else. This feature rules out the applicability of existing equivalence results in the Dolev-Yao model. The analysis of security protocols under the Multi-Attacker threat model brings forward yet more insights, such as retaliation attacks and anticipation attacks, which formalise currently realistic scenarios of principals competing each other for personal profit. They are variously demonstrated on a classical protocol, Needham-Schroeder??s, and on a modern deployed protocol, Google??s SAML-based single sign-on protocol. The general threat model for security protocols based on set-rewriting that was adopted in AVISPA (Armando et al. 2005) is extended to formalise the Multi-Attacker. The state-of-the-art model checker SATMC (Armando and Compagna, Int J Inf Secur 6(1):3?C32, 2007) is then used to automatically validate the protocols under the new threats, so that retaliation and anticipation attacks can automatically be found. The tool support scales up to the Multi-Attacker threat model at a reasonable price both in terms of human interaction effort and of computational time.