Search

The logic-programming paradigm is a prime example of how the integration of the declarative and the operational aspects of logical systems can be used to provide a unied framework for both specication and programming languages. In essence, programming in logic amounts to giving appropriate axiomatic formalizations of computable functions, which can then be executed by means of carefully designed goal-directed deduction rules. In this thesis, we examine common features of various conventional logicprogramming languages, ranging from the most traditional variant of the paradigm - dened over Horn-clause logic - to rst-order and higher-order equational logic programming. Based on these, we propose an abstract model-theoretic framework that allows us to develop and conduct research into logic programming over an arbitrary logical system, without concrete models, sentences, satisfaction, or deduction, and thus to explore the logicprogramming paradigm for other, less conventional formalisms, like the logic of orchestration schemes used in the context of service-oriented computing. Our study is based on abstractions of notions such as logic program, clause, query, solution, and computed answer, which we develop over Goguen and Burstall's theory of institutions. These give rise to a series of concepts that formalize the interplay between the denotational and the operational semantics of logic programming. We investigate properties concerning the satisfaction of quantied sentences, discuss a variant of Herbrand's theorem that is not limited in scope to any logical formalism or construction of logic programs, and dene a sound and conditionally complete procedure for computing solutions to queries. Within this setting, we further examine two of the most fundamental aspects of the modularization of logic programs - the preservation and the reection of solutions along morphisms of programs - leading to results that can be applied not only to unstructured logic programs (plain sets of clauses), but also to elaborate module systems.

We discuss P#, our implementation of a tool which allows interoperation between a concurrent superset of the Prolog programming language and C#. This enables Prolog to be used as a native implementation language for Microsoft's .NET platform. P# compiles a linear logic extension of Prolog to C# source code. We can thus create C# objects from Prolog and use C#'s graphical, networking and other libraries. P# was developed from a modified port of the Prolog to Java translator, Prolog Cafe. We add language constructs on the Prolog side which allow concurrent Prolog code to be written. We add a primitive predicate which evaluates a Prolog structure on a newly forked thread. Communication between threads is based on the unification of variables contained in such a structure. It is also possible for threads to communicate through a globally accessible table. All of the new features are available to the programmer through new built-in Prolog predicates. We present three case studies. The first is an application which allows several users to modify a database. The users are able to disconnect from the database and to modify their own copies of the data before reconnecting. On reconnecting, conflicts must be resolved. The second is an object-oriented assistant, which allows the user to query the contents of a C# namespace or Java package. The third is a tool which allows a user to interact with a graphical display of the inheritance tree. Finally, we optimize P#'s runtime speed by translating some Prolog predicates into more idiomatic C# code than is produced by a naive port of Prolog Cafe. This is achieved by observing that semi-deterministic predicates (being those which always either fail or succeed with exactly one solution) that only call other semi-deterministic predicates enjoy relatively simple control flow. We make use of the fact that Prolog programs often contain predicates which operate as functions, and that such predicates are usually semi-deterministic.

PrologPF is a parallelising compiler targeting a distributed system of general purpose workstations connected by a relatively low performance network. The source language extends standard Prolog with the integration of higher-order functions. The execution of a compiled PrologPF program proceeds in a similar manner to standard Prolog, but uses oracles in one of two modes. An oracle represents the sequence of clauses used to reach a given point in the problem search tree, and the same PrologPF executable can be used to build oracles, or follow oracles previously generated. The parallelisation strategy used by PrologPF proceeds in two phases, which this research shows can be interleaved. An initial phase searches the problem tree to a limited depth, recording the discovered incomplete paths. In the second phase these paths are allocated to the available processors in the network. Each processor follows its assigned paths and fully searches the referenced subtree, sending solutions back to a control processor. This research investigates the use of the technique with a one-time partitioning of the problem and no further scheduling communication, and with the recursive application of the partitioning technique to effect dynamic work reassignment. For a problem requiring all solutions to be found, execution completes when all the distributed processors have completed the search of their assigned subtrees. If one solution is required, the execution of all the path processors is terminated when the control processor receives the first solution. The presence of the extra-logical Prolog predicate cut in the user program conflicts with the use of oracles to represent valid open subtrees. PrologPF promotes the use of higher-order functional programming as an alternative to the use of cut. The combined language shows that functional support can be added as a consistent extension to standard Prolog.

This research develops a scheme for the efficient execution of Prolog programs on a distributed memory parallel machine. Efficient schemes for the sequential execution of Prolog are generally based on the Warren Abstract Machine ('WAM') [Warren 1983]; our execution scheme places an extended 'WAM' on each processor which can receive tasks and spawn further tasks to other processors. The extended 'WAM' supports independent and-parallel execution and intelligent backtracking at the clause level. An analysis of binding communication between processors is made to select the most efficient scheme. Additional run-time information can be derived from the communication of bindings at no additional overhead. An extended 'WAM' instruction set is designed where information provided at compile-time is combined with information derived at run-time to dynamically determine the data-dependencies between subgoals. A scheme for intelligent backtracking in parallel clauses is developed which both `intelligently' selects the redo subgoal(s) and allows other execution in the clause to persist unless bindings are directly affected by the redo. Potentially, parallel execution can continue in a clause when backtracking occurs. The dynamic information is also used to prune unnecessary search space and an optimisation, `intelligent cutting' is introduced. A distributed Prolog executor has been implemented for an array of transputer processing elements. A complete analysis of the implementation is made for both sequential and parallel execution. Performance results are comparable with other results in the literature for shared memory architectures.

The general area of developing, applying and studying new and parallel models of computation is motivated by a need to overcome the limits of current Von Neumann based architectures. A key area of research in understanding how new technology can be applied to Al problem solving is through using logic languages. Logic programming languages provide a procedural interpretation for sentences of first order logic, mainly using a class of sentence called Horn clauses. Horn clauses are open to a wide variety of parallel evaluation models, giving possible speed-ups and alternative parallel models of execution. The research in this thesis is concerned with investigating one class of parallel logic language known as Committed Choice Non-Deterministic languages. The investigation considers the inherent parallel behaviour of Al programs implemented in the CCND languages and the effect of various alternatives open to language implementors and designers. This is achieved by considering how various Al programming techniques map to alternative language designs and the behaviour of these Al programs on alternative implementations of these languages. The aim of this work is to investigate how Al programming techniques are affected (qualitatively and quantitatively) by particular language features. The qualitative evaluation is a consideration of how Al programs can be mapped to the various CCND languages. The applications considered are general search algorithms (which focuses on the committed choice nature of the languages); chart parsing (which focuses on the differences between safe and unsafe languages); and meta-level inference (which focuses on the difference between deep and flat languages). The quantitative evaluation considers the inherent parallel behaviour of the resulting programs and the effect of possible implementation alternatives on this inherent behaviour. To carry out this quantitative evaluation we have implemented a system which improves on the current interpreter based evaluation systems. The new system has an improved model of execution and allows several

This thesis is concerned with the validation of chess endgame strategies. It is also concerned with the synthesis of strategies that can be validated. A strategy for a given player is the specification of the move to be made by that player from any position that may occur. This move may be dependent on the previous moves of both sides. A strategy is said to be correct if following the strategy always leads to an outcome of at least the same game theoretic value as the starting position. We are not concerned with proving the correctness of programs that implement the strategies under consideration. We shall be working with knowledge-based programs which produce playing strategies, and assume that their concrete implementations (in POP2, PROLOG etc.) are correct. The synthesis approach taken attempts to use the large body of heuristic knowledge and theory, accumulated over the centuries by chessmasters, to find playing strategies. Our concern here is to produce structures for representing a chessmaster's knowledge wnich can be analysed within a game theoretic model. The validation approach taken is that a theory of the domain in the form of the game theoretic model of chess provides an objective measure of the strategy followed by a program. Our concern here is to analyse the structures created in the synthesis phase. This is an instance of a general problem, that of quantifying the performance of computing systems. In general to quantify the performance of a system we need,- A theory of the domain. - A specification of the problem to be solved. - Algorithms and/or domain-specific knowledge to be applied to solve the problem.

Cognitive Science attempts to study entities which in some sense possess beliefs, intentions, desires etc. The preferred term in this thesis for such entities is agents. An attempt at a scientific analysis of agents however throws up a number of questions. What are the right concepts to describe agents? What kinds of formal notations permit perspicuous reasoning about agents? What can be said about the architecture and construction of agents? The introductory section of this thesis discusses these questions in some detail, using Dennett's ideas about intentional systems [Den87] as a point of departure. I then examine a number of studies from Artificial Intelligence, Logic, Natural Language semantics and Philosophy which give shape to the current state of the art in agent theory. This leads to the development of a mathematical model of multi-object/agent interaction, which I call the SRS-model (SRS - Synchronous Reactive Systems). I demonstrate the adequacy of the model by using it to formalise learning and games scenarios. Next, various logics are introduced which capture input-output and then belief-desire level descriptions of agents. These logics are given an SRS-model semantics, and adequacy is shown by modelling a psychological experiment (an agent in a Skinner Box). It is shown how the example can be formally analysed in terms of mechanisms and architecture at the SRS-level (including a computer simulation); at the level of behaviourism (using a temporal logic - APTL); and at an intentional level (using an epistemic-conative temporal logic ECTL). Some remarks are made about extending the analysis to multi-agent situations involving co-operation, competition and dialogue. Finally, a detailed survey is made of the main mathematical and logical resources available to the style of formal cognitive science advocated in this thesis. I include modal logic, including its epistemic and doxastic variants; the extension of modal logic to dynamic logic; and the various approaches recently developed in the logic of time.

The field of Artificial Intelligence is fundamentally about designing computer programs (called agents) in an architecture that they are empowered to make more complex decisions than what could be done before. One such decision area considers planning a sequence of actions to achieve a predetermined goal. Planning becomes more complex when the agent's environment changes, or when an agent's attempt to perform actions fails. While many agent architectures have been proposed to accomplish this kind of task before, the Architecture for Intentional Agents (AIA) seems most promising. However, AIA has limitations in a desirable decision area: AIA is incapable of determining whether actions conform to rules (called policies) provided by an external agent controller. Policies can be expressed in the Authorization and Obligation Policy Language (AOPL) as an allowance to perform an action (an authorization) or a requirement to perform an action (an obligation). We extend AIA such that it can reason over compliance with AOPL policies and abide by them. This extended architecture, called APIA, is evaluated by examples that demonstrate its policy compliance as well as by its runtime performance.

In the past, the semantic issues raised by the non-monotonic nature of aggregates often prevented their use in the recursive statements of logic programs and deductive databases. However, the recently introduced notion of Pre-Mappability (PreM) has shown that, in key applications of interest, aggregates can be used in recursion to optimize the perfect-model semantics of aggregate-stratified programs. Therefore, we can preserve the declarative formal semantics of such programs, while achieving a highly efficient operational semantics that is conducive to scalable implementations on parallel and distributed platforms. In this work, we show that using PreM, a wide spectrum of classical algorithms, ranging from graph analytics and dynamic programming based optimization problems to data mining, machine learning and online streaming applications can be concisely expressed in declarative languages by using aggregates in recursion. We present a concise analysis of this very general property and characterize its different manifestations for different constraints and rules. Next, we prove that PreM-optimized plans are easily parallelizable and produce the same results as the single executor programs. Thus, PreM can be trivially assimilated into the data-parallel computation plans of different distributed systems, irrespective of whether these follow bulk synchronous parallel (BSP) or asynchronous computing models. This makes possible many advanced BigData applications to be now expressed declaratively in logic-based languages, including Datalog, Prolog, and even SQL, while enabling their execution with superior performance and scalability as compared to other specialized systems. Furthermore, we show that under PreM nonlinear recursive queries can be evaluated using a hybrid stale synchronous parallel (SSP) model with relaxed synchronization on distributed environments. We present empirical evidence of its benefits. We also compare the usability, expressivity and performance of PreM-optimized queries with queries written in quasi-declarative programming methodologies inspired by procedural languages like XY-stratification to showcase the different trade-offs and ramifications associated with each. Lastly, we present robust online optimization techniques using two popular case studies, namely online lossless frequent pattern mining and online decision tree construction, to show how compact representations and statistical approximations can deliver superior performances in real-time for several streaming data mining and machine learning applications.

The mental attitudes, such as belief, desire, and intention, play a central role in the design and implementation of autonomous agents. In 1987, Bratman proposed a so-called belief-desire-intention (BDI) theory which inspired a multitude of BDI logics and BDI architectures. Bratman highlighted the fundamental role of an agent's future-directed intentions: they are high-level plans to which the agent is committed. Such high-level plans cannot be executed directly: they have to be stepwise refined into more elaborated plans. Ideally the plans at the end of the refinement process contain only basic actions which the agent can perform directly. The process of intention refinement is crucial to the BDI theory and every step of refinement establishes a means-end relation between the refined intentions and the intentions refining it. However, there are very few accounts of hierarchical intention refinement in the existing BDI logics. The concept of automated planning is central in Bratman's theory. As a traditional research community of artificial intelligence, automated planning has attracted numerous attentions and it has already been integrated into BDI architectures. In particular, the way of generating solutions in hierarchical task network (HTN) planning is refining high-level actions step-by-step until basic actions. Thus, the idea of HTN planning should be revelent for BDI agents. However, except for the line of work of de Silva and Sardina et al., hierarchical intention refinement has been scarcely considered in the existing BDI agents. The aim of this thesis is to provide a logic-based comprehensive analysis of the hierarchical refinement process. In this thesis, intention refinement is considered from two perspectives: the entailment and the primitive. From the former, intentions are managed in a co-called belief-intention database where refinement is addressed via the logical entailment based on the action law; while from the latter, refinement is defined in an explicit and static way, just as in HTN planning. From the entailment perspective, this thesis starts with an extension of Shoham's database framework on beliefs and intentions by introducing the notions of high-level intentions and environmental events. In a belief-intention database, a set of intentions can refine an intention if the set is minimal and suffices to guarantee the satisfaction of the intention. This thesis also investigates the complexity of the decision problems of satisfiability, consequence, refinement, instrumentality in the proposed database framework, which are all PSPACE-complete. Furthermore, this thesis explores the relations between the database framework and two logics: propositional linear temporal logic and dynamic logic with propositional assignment. The reductions to these two logics contribute to finding a set of intentions to refine a high-level intention via invoking the automated tools for these two logics. From the primitive perspective, this thesis provides a logical semantics for HTN planning based on propositional dynamic logic. In the dynamic framework, refinement is captured by the program inclusion operator. By equipping high-level actions with pre- and post-condition, a coherence condition for HTN domains is proposed to evaluate the correctness of the predefined refinement methods. Moreover, the postulates of soundness and completeness for high-level actions are given under the dynamic semantics. When it comes to the completeness, it is usually a big challenge to define all possible refinement methods in HTN planning. It is promising to relax some restrictions on solutions: Geier & Bercher's HTN planning with task insertion (TIHTN) allows solutions obtained by inserting actions. To capture the pre- and post-condition of actions, this thesis further extends TIHTN by introducing state constraints and calls the extension TIHTNS planning. It has been shown that the property of acyclic decomposition still holds in TIHTNS planning and then an acyclic progression operator for finding a plan is proposed. Based on the progression operator, it is proved that the additional consideration of state constraints does not increase the complexity of the plan-existence problem, staying in 2-NEXPTIME-complete.

Answer set programming (ASP) is a declarative programming paradigm for the design and implementation of knowledge-intensive applications, particularly useful for modeling problems involving combinatorial search. The input languages of the first ASP software systems had the attractive property of a simple, fully specified declarative semantics, making it possible to use formal methods to analyze ASP programs -- to verify correctness, for example, or to show that two programs were equivalent. Since that time, many useful new constructs have been added to input languages. The increase in usability, however, has come at the expense of a fully specified semantics, as the semantics of newer constructs has not quite kept pace with the most general syntax that solvers can handle. In this thesis, we will describe one approach to bridging the gap between mathematical formulations of the semantics of ASP languages and the current state of the languages themselves. Our approach is to view ASP programs as corresponding to infinitary formulas (formulas with infinitely long conjunctions and disjunctions).

Advanced analytics are used to discover hidden patterns and trends in massive datasets. Great strides have been made by researchers to provide computational models, systems and accompanying languages for analytics. However, there is still a dire need for highly expressive declarative languages that enable the compilation, optimization and evaluation of advanced analytics over massive datasets. Specifically, a language for analytics needs (i) to support the expression of analytics over multiple data models (ii) to provide high-level declarative constructs enabling system optimizations, and (iii) be conducive for iterative or recursive evaluation.In this dissertation, we propose an expressive Datalog language for advanced analytics, and compilation and optimization techniques for its efficient evaluation on systems designed for iterative execution. Specifically, this dissertation makes two main contributions:(i) We develop and demonstrate a next generation Datalog System - the Deductive Application Language System (DeALS). To extend the range of analytics supported in DeALS, we add support for aggregation in recursion into our logic-based language. We propose the design and implementation of several monotonic aggregates that can be used in recursive Datalog rules and evaluated efficiently using our novel optimization techniques. We demonstrate the effectiveness of these aggregates and conduct an experimental comparison with other Datalog systems and determine that DeALS combines superior generality with superior performance.(ii) We design and implement BigDatalog, a Datalog system on Apache Spark, for large-scale advanced analytics. We implement BigDatalog for efficient distributed evaluation and to utilize communication-reduction techniques during evaluation. We propose compilation and optimization techniques, as well as job scheduling techniques, to support efficiently the evaluation of DeAL programs on Spark. We conduct an experimental comparison with other state-of-the-art large-scale Datalog systems and demonstrate the efficacy of our techniques and effectiveness of our Spark extensions in supporting Datalog-based analytics.

Constraint answer set programming (CASP) is a declarative problem solving paradigm that combines the strengths of answer set programming (ASP) and constraint programming (CP). ASP solvers provide good computational performance by conflict-driven nogood learning (CDNL) and exploiting unfounded sets. To model features like finite domain variables and global constraints, which are naturally dealt with in CP, hybrid CASP systems have been developed that delegate CP constructs to a CP solver. While this achieved some success, hybrid systems do not seamlessly integrate with CDNL. We address this deficiency by devising two alternative approaches that accommodate CDNL. For one, we introduce a translation-based approach. The idea is to enhance ASP with CP constructs through translation to ASP. Implemented as preprocessing, this allows us to apply existing CDNL-enabled ASP systems to CASP solving. Our contributions include various generic translations that work for any constraint, and specialised encodings for important global constraints such as ALL-DIFFERENT, GRAMMAR, and REACHABILITY. We show that the inference of ASP solvers can simulate the effect of complex CP algorithms in many cases. Propagation of REACHABILITY, however, can be hindered because ASP systems disregard some consequences from unfounded sets for performance reasons. We tackle this weakness by providing more efficient methods using a reduction to the problem of finding dominators in a flowgraph. For another, we devise an extension to CDNL-based ASP solving that can integrate CP constructs via lazy nogood generation (LNG). Rather than a-priori translations into ASP, the idea of LNG is to make necessary parts of an encoding explicit on demand and only when new information can be propagated. We introduce external propagators to facilitate LNG and incorporate them into a decision procedure for ASP solving that is centred around CDNL. We then demonstrate how to seamlessly integrate constraint propagation with this framework, resulting in a novel approach to CASP solving. We have implemented a prototypical CASP system to demonstrate some key principles of our approaches. In 2013, it has successfully participated in a model and solve competition, outperforming hybrid systems.

Knowledge about actions is an important part of commonsense knowledge studied in Artificial Intelligence. For decades, researchers have been developing methods for describing how actions affect states of the world and for automating reasoning about actions. In recent years, significant progress has been made. In particular, the frame problem has been solved using nonmonotonic knowledge representation formalisms, such as logic programming under the answer set semantics. New theories of causality have allowed us to express causal dependencies between fluents, which has proved essential for solving the ramification problem. It has been shown that reasoning about actions described by logic programs and causal theories can be automated using answer set programming. Action description languages are high level languages that allow us to represent knowledge about actions more concisely than when logic programs are used. Many action description languages have been described in the literature, including B, C, and C+. Reasoning about dynamic domains described in languages C and C+ can be performed automatically using the Causal Calculator (CCalc), which employs SAT solvers for search, and the systems coala and cplus2asp, which employ answer set solvers such as clingo. The dissertation addresses problems of three kinds. First, we study some mathematical properties of expressive action languages based on nonmonotonic causal logic that were not well understood until now. This includes causal rules expressing synonymy, nondefinite causal rules, and nonpropositional causal rules. We generalize existing translations from nonmonotonic causal theories to logic programming under the answer set semantics. This makes it possible to automate reasoning with a wider class of causal theories by calling answer set solvers. Second, we design and study a new action language BC, which is more expressive in some ways than the existing and previously proposed languages. We develop a framework that combines the most useful expressive features of the languages B and C+, and use program completion to characterize the effects of actions described in these languages. Third, we illustrate the possibilities of the new action language by two practical applications: to the dynamic domain of the Reactive Control System of the space shuttle, and to the task planning of mobile robots.

As an expressive knowledge representation language for Semantic Web, Web Ontology Language (OWL) plays an important role in areas like science and commerce. The problem of maintaining integrity constraints arises because OWL employs the Open World Assumption (OWA) as well as the Non-Unique Name Assumption (NUNA). These assumptions are typically suitable for representing knowledge distributed across the Web, where the complete knowledge about a domain cannot be assumed, but make it challenging to use OWL itself for closed world integrity constraint validation. Integrity constraints (ICs) on ontologies have to be enforced; otherwise conflicting results would be derivable from the same knowledge base (KB). The current trends of incorporating ICs into OWL are based on its query language SPARQL, alternative semantics, or logic programming. These methods usually suffer from limited types of constraints they can handle, and/or inherited computational expensiveness. This dissertation presents a comprehensive and efficient approach to maintaining integrity constraints. The design enforces data consistency throughout the OWL life cycle, including the processes of OWL generation, maintenance, and interactions with other ontologies. For OWL generation, the Paraconsistent model is used to maintain integrity constraints during the relational database to OWL translation process. Then a new rule-based language with set extension is introduced as a platform to allow users to specify constraints, along with a demonstration of 18 commonly used constraints written in this language. In addition, a new constraint maintenance system, called Jena2Drools, is proposed and implemented, to show its effectiveness and efficiency. To further handle inconsistencies among multiple distributed ontologies, this work constructs a framework to break down global constraints into several sub-constraints for efficient parallel validation.

Answer Set Programming (ASP) is a form of declarative programming oriented towards difficult and primarily NP-hard search problems. Generally speaking, an ASP search problem is formulated as a theory of some language of formal logic. The formalization is designed in such a way that the problem description is usually separate from the problem instance. Thus, once a particular encoding of a problem instance is combined with the problem description, it results in some theory of formal logic whose models (under a particular semantics) corresponds to a solution of the problem instance. This thesis is about the translation of ASP programs into classical first-order logic theories. Viewed in the context of expressing logic programs with variables into (classical) first-order logic, work of this direction goes all the way back to Clark who gave us what is now called the Clark’s completion semantics, on which this work is based. This work modifies the Clark’s completion in such a way that the models of the modified completion corresponds exactly to the answer sets. We then report on such an implementation of grounding completely on first-order theories rather than on programs (i.e., as is the case with traditional ASP solvers), and show that the new approach is quite competitive with current effective solvers on very large instances of the Hamiltonian circuit program. In addition, we further consider the translation of logic programs with aggregates (a very important building block of ASP) under the stable model semantics, into classical first-order theories. Preferences play an important role in knowledge representation and reasoning. In the past decade, a number of approaches for handling preferences have been developed in various nonmonotonic reasoning formalisms, while adding preferences into ASP has been known to have promising advantages from both implementation and application viewpoints. This thesis also extends the notion of preferred ASP (i.e., answer set programming with preferrence relations among the rules), that is currently only formalized for propositional programs, into the notion of first-order ASP. To this aim, we develop both a (first-order) fixpoint type characterization that is similar to Zhang and Zhou’s progression semantics, and a classical logic formulation so that the preferred answer sets are exactly those models of the logic formula. We further show that the fixpoint type characterization and classical logic formulation coincide.

The Extensible Markup Language (XML) has widely become the de facto method for the encoding of stored and shared computer data. Many of today's Internet applications utilise XML for the exchange of information. In many cases, information that is stored in XML can be regarded as sensitive or private (ie. personal, financial, or generally classified information). For this reason there is an obvious necessity to ensure that information that is deemed sensitive or private is protected with a method of security or access control. In this thesis we investigate and present such a method with the introduction of a formal language that can provide an authoritative framework for XML documents. In conjunction with the highly regarded and recognised Role-based Access Control (RBAC) model, we designed a formal language of authorisation for XML documents. With the inherent features of the RBAC model (such as subject and role based structuring, authorisation delegation and propagation, conflict resolution, separation of duty), we developed Axml(T), a formal language capable of specifying a queryable security policy base. Beyond this, we also furthered its expressive nature and capabilities by also incorporating Temporal Logic. This gives Axml(T) the ability to specify and reason upon access control temporally and is something that is rarely implemented in terms of authorisation languages. For the foundation and semantics of Axml(T), we turned to a relatively new and commonly used form of declarative programming used in Knowledge Representation and Logic Programming. Answer Set Programming (ASP) provides Axml(T) with a semantic definition and translation so that we can treat our security policy base as a logic program. This logic program translation is reasoned upon to provide an answer set (stable model) which dictates the authorisations to XML documents. As well as the description and presentation of this formal language, we also produced a software implementation to demonstrate its use and features. Using case studies, we show a level of complexity that can be accomplished by using Axml(T) to specify access control to XML documents. Finally, we also present further extensions and theories to the formal language that increase its capabilities and expressiveness and also further differentiate it from other research in XML security. These extensions, such as query containment and aggregates, increase the complexity in which Axml(T) can specify authorisation to XML documents. We formally define these extensions in Axml(T) and demonstrate them through further examples.

The aim of this thesis is to develop faster method for stable model computation of non-stratified logic programs and study its efficiency. It focuses mainly on the stable model and weak well founded semantics of logic programs. We propose an approach to compute stable models by where we first transform the logic program using paraconsistent relational model, then we compute the weak-well founded model which is used to generate a set of models consisting of the true and unknown values, which are tested for stability. We perform some experiments to test the efficiency of our approach which incurs overhead to eliminate negative values against a Naïve method of stable model computation.

Abstract: Answer set programming (ASP), namely logic programming under the answer set semantics, provides a promising constraint programming paradigm, due to its simple syntax, high expressiveness, and effective computational properties. This programming paradigm can be viewed as a variant of SAT. A main drawback of ASP, like SAT, is that the framework is primarily formulated for reasoning with individuals, where each is represented by an atom in the traditional sense. Recently, ASP has been extended to include constraints to facilitate reasoning with sets of atoms in an explicit manner. These constraints include weight constraints, aggregates, and abstract constraints. Logic programs with these constraints are referred to as weight constraint, aggregate and abstract constraint programs. We investigate the properties and computations of weight constraint, aggregate, and abstract constraint programs, respectively. For properties, we improve the formulation of loop formulas for weight constraint and aggregate programs, propose loop formulas for abstract constraint programs, and characterize strong equivalence of these programs. For computations, we refine the existing constraint propagation mechanism in the computation of weight constraint programs and advocate a new approach to computing aggregate programs.

Answer set programming (ASP) is a declarative programming paradigm oriented towards difficult combinatorial search problems. Syntactically, ASP programs look like Prolog programs, but solutions are represented in ASP by sets of atoms, and not by substitutions, as in Prolog. Answer set systems, such as Smodels, Smodelscc, and DLV, compute answer sets of a given program in the sense of the answer set (stable model) semantics. This is different from the functionality of Prolog systems, which determine when a given query is true relative to a given logic program. ASP has been applied to many areas of science and technology, from the design of a decision support system for the Space Shuttle to graph-theoretic problems arising in zoology and linguistics. The "native" answer set systems mentioned above are based on specialized search procedures. Usually these procedures are described fairly informally with the use of pseudocode. We propose an alternative approach to describing algorithms of answer set solvers. In this approach we specify what "states of computation" are, and which transitions between states are allowed. In this way, we define a directed graph such that every execution of a procedure corresponds to a path in this graph. This allows us to model algorithms of answer set solvers by a mathematically simple and elegant object, graph, rather than a collection of pseudocode statements. We use this abstract framework to describe and prove the correctness of the answer set solver Smodels, and also of Smodelscc, which enhances the former using learning and backjumping techniques. Answer sets of a tight program can be found by running a SAT solver on the program's completion, because for such a program answer sets are in a one-to-one correspondence with models of completion. SAT is one of the most widely studied problems in computational logic, and many efficient SAT procedures were developed over the last decade. Using SAT solvers for computing answer sets allows us to take advantage of the advances in the SAT area. For a nontight program it is still the case that each answer set corresponds to a model of program's completion but not vice versa. We show how to modify the search method typically used in SAT solvers to allow testing models of completion and employ learning to utilize testing information to guide the search. We develop a new SAT-based answer set solver, called Cmodels, based on this idea. We develop an abstract graph based framework for describing SAT-based answer set solvers and use it to represent the Cmodels algorithm and to demonstrate its correctness. Such representations allow us to better understand similarities and differences between native and SAT-based answer set solvers. We formally compare the Smodels algorithm with a variant of the Cmodels algorithm without learning. Abstract frameworks for describing native and SAT-based answer set solvers facilitate the development of new systems. We propose and implement the answer set solver called SUP that can be seen as a combination of computational ideas behind Cmodels and Smodels. Like Cmodels, solver SUP operates by computing a sequence of models of completion of the given program, but it does not form the completion. Instead, SUP runs the Atleast algorithm, one of the main building blocks of the Smodels procedure. Both systems Cmodels and SUP, developed in this dissertation, proved to be competitive answer set programming systems.

The aim of this thesis is to study the role played by negation in databases and to develop data models that can handle inconsistent and incomplete information. We develop models that also allow incompleteness through disjunctive information under both the CWA and the OWA in relational databases. In the area of logic programming, extended logic programs allow explicit representation of negative information. As a result, a number of extended logic programs have an inconsistent semantics. We present a translation of extended logic programs to normal logic programs that is more tolerant to inconsistencies. Extended logic programs have also been used widely in order to compute the repairs of an inconsistent database. We present some preliminary ideas on how source information can be incorporated into the repair program in order to produce a subset of the set of all repairs based on a preference for certain sources over others.

At Ctest Laboratories we are exploring the notion of automated conversion of the semi-structured text to an epistemic structure suitable for deductive inference. In this paper we will develop an epistemic structured representation for electronic transcripts ofinterrogative domains. We propose that knowledge which is typically not visible to keyword search or string matching, can be readily extracted from the an electronic transcript when it is given an appropriate epistemic structure. We introduce an Epistemic Structure Es and a process for converting a semi-structured transcript from and interrogative domain to Es. In this paper we restrict our discussion and analysis to transcripts that have been stored as semi-structured text. In particular we are interested in any knowledge that can be deduced by an interrogative agent from the content of an electronic transcript. Further we develop the notion of an interrogative agent that relies on epistemic justification as a condition for knowledge.

Logic programming with answer set semantics has been considered appealing rule-based formalism language and applied in information security areas. In this thesis, we investigate the problems of authorization in distributed environments and security protocol verification and update. Authorization decisions are required in large-scale distributed environments, such as electronic commerce, remote resource sharing, etc. We adopt the trust management approach, in which authorization is viewed as a ‘proof of compliance" problem. We develop an authorization language AL with non-monotonic feature as the policy and credential specification language, which can express delegation with depth control, complex subject structures, both positive and negative authorizations, and separation of duty concepts. The theoretical foundation for language AL is the answer set semantics of logic programming. We transform AL to logic programs and the authorization decisions are based on answer sets of the programs. We also explore the tractable subclasses of language AL. We implement a fine grained access control prototype system for XML resources, in which the language AL¤ simplified from AL is the policy and credential specification language. We define XPolicy, the XML format of AL¤, which is a DTD for the XML policy documents. The semantics of the policy is based on the semantics of language AL. The system is implemented using Java programming. We investigate the security protocol verification problem in provable security approach. Based on logic programming with answer set semantics, we develop a unified framework for security protocol verification and update, which integrates protocol specification, verification and update. The update model is defined using forgetting techniques in logic programming. Through a case study protocol, we demonstrate an application of our approach.

As information systems evolve to cope with the ever increasing demand of today’s digital world, so does the need for more effective means of protecting information. In the early days of computing, information security started out as a branch of information technology. Over the years, several advances in information security have been made and, as a result, it is now considered a discipline in its own right. The most fundamental function of information security is to ensure that information flows to authorised entities, and at the same time, prevent unauthorised entities from accessing the protected information. In a typical information system, an access control system provides this function. Several advances in the field of information security have produced several access control models and implementations. However, as information technology evolves, the need for a better access control system increases. This dissertation proposes an effective, yet flexible access control system: the Policy Updater access control system. Policy Updater is a fully-implemented access control system that provides policy evaluations as well as dynamic policy updates. These functions are provided by the use of a logic-based language, L, to represent the underlying access control policies, constraints and policy update rules. The system performs authorisation query evaluations, as well as conditional and dynamic policy updates by translating language L policies to normal logic programs in a form suitable for evaluation using the well-known Stable Model semantics. In this thesis, we show the underlying mechanisms that make up the Policy Updater system, including the theoretical foundations of its formal language, the system structure, a full discussion of implementation issues and a performance analysis. Lastly, the thesis also proposes a non-trivial extension of the Policy Updater system that is capable of supporting temporal constraints. This is made possible by the integration of the well-established Temporal Interval Algebra into the extended authorisation language, language LT , which can also be translated into a normal logic program for evaluation. The formalisation of this extension, together with the full implementation details, are included in this dissertation.

In this dissertation we show how conflict clause learning, a technique that has been very useful in improving the efficiency of Boolean logic satisfiability search, can be adapted to speed up dramatically the search for models of answer set programs.Answer set programming is a knowledge representation paradigm related to the areas of logic programming and nonmonotonic reasoning. Many of the applications of answer set programming come from the areas of artificial intelligence – related diagnosis and planning. The problem of finding an answer set for a normal or extended logic program is NP-hard. Current complete answer set solvers are patterned after the Davis-Putnam-Loveland-Logemann (DPLL) algorithm for solving Boolean satisfiability (SAT) problems, but are adapted to the nonmonotonic semantics of answer set programming.Recent SAT solvers include improvements to the DPLL algorithm. Conflict clause learning has been particularly effective in this regard. A conflict clause represents a backtracking solver's analysis of why a conflict occurred. This analysis can be used to further prune the search space and to direct the search heuristic. The use of such clauses has improved significantly the efficiency of satisfiability solvers over the past few years, especially on structured problems arising from applications.In this dissertation we describe how we have adapted conflict clause techniques for use in the answer set solver Smodels . We experimentally compare the performance of the resulting program, Smodels cc, to that of the original Smodels program. Our tests show dramatic speedups for Smodelscc on a wide range of problems.We also compare the performance of Smodelscc with that of two other recent answer set solvers, ASSAT and Cmodels-2. ASSAT and Cmodels-2 directly call Boolean satisfiability solvers in order to search for answer sets. On so-called “non-tight” problems, Smodelscc showed substantially better performance than these solvers. The performance advantage that Smodelscc enjoys on non-tight problems is due to the unfounded set test that Smodelscc inherits from the Smodels solver, and the fact that this test is executed frequently throughout the program's search for answer sets.

This research concentrates on the optimization of Constraint Logic Programming, or CLP, languages, and in particular, a significant class of optimizations that focus on program loops. Declarative systems represent loop state by chains of variables, whether in call stack frames, or the rows of a system of equations, and the time costs are significant compared to imperative languages that can reuse variables during iteration. In particular, some procedures add numerical constraints to the solver in a predictable pattern, using far less than the full power of the constraint solver. We wish to optimize these chains of constraints, or threads . We use a matrix-vector pair, an affine transform , to represent the incremental computation that occurs at each iteration of a recursive predicate. By the associativity of transform multiplication, we may compose a chain of ground transforms prior to their application to program variables. The accumulated composition is then applied to relate the procedure parameters in a single step outside the loop, reducing the number of solver calls from O(n) to O(1). An implementation of the thread optimization for a CLP system requires compile-time analysis, source translation, and specialized code generation. We modify an existing CLP compiler, CLPR , to add the analysis, translation and code generation phases, and run timing tests to determine the actual speedup. This work defines and proves correct a broad class of CLP optimizations, the thread optimizations, which apply to a wide variety of recursive procedures in any practical CLP language; describes our implementation of the thread optimization of numeric constraints, for an instance of the CLP family, CLPR; and demonstrates that this implementation achieves a significant speedup for optimized programs.

This thesis presents the Planning System DLVK, which supports the novel Planning Language K. The language allows to represent AI planning problems in a declarative way and is capable of representing incomplete knowledge as well as nondeterministic effects of actions.After explaining some basics, the syntax and semantics of this language will be formally described and some results on the computational complexity of our language will be given, proving that K is capable of expressing hard planning problems, possibly involving incomplete knowledge or uncertainty, such as secure (conformant) planning.A translation from various planning tasks specified in K to a logic programming framework will be shown subsequently. We have implemented a prototype of a planning system, DLVK, on top of the disjunctive logic programming system DLV, to show the practical use of our translation. This prototype will be presented in detail. Finally, examples and experimental results will be given, together with an outlook to further research.

Knowledge representation and inference are the backbone of artificial intelligence, and logic programming is one of the most widely used knowledge representation tools. Logic programming with deduction/induction/abduction as the reasoning technique is serving numerous fields of artificial intelligence. In dynamic domains where there are constant changes in knowledge, updating the knowledge base is crucial to keep it stable. This thesis investigates the issues in updating the knowledge base. Two types of logic program based updates are considered, simple fact based updates where the knowledge base is updated by a simple fact, and rule based updates where the knowledge base is updated by a rule. A SLDNF based procedural approach is proposed to implement such updates. This thesis also investigates the issues involved in simple fact based and rule based abduction, and it is observed that updates are closely related to abduction. A SLDNF based procedural approach to perform simple fact/rule based updates and abduction is proposed as a result of this study

This thesis is concerned with constraint-based logical and computational frameworks for resolving and relaxing over-constrained systems. The context is provided by two such frameworks, Hierarchical Constraint Logic Programming (HCLP) and Partial Constraint Satisfaction Problem techniques (PCSP), both of which have been extensively discussed in the literature. Our work is driven by the reasons why over-constrained systems arise, the characteristics of the 'ideal' paradigm for resolving them, and the issue of compositionality which is very important in general if we wish to examine large systems by examining and then combining smaller parts. We abstract away from programming language issues in order to focus on constraint solving. The main original work of this thesis is divided into three parts. Firstly we present a complete method for transforming between the HCLP and PCSP representations of a problem, thus showing that theoretically they have equivalent expressive power. Secondly, having discussed compositionality in general, we present a two-stage variant of HCLP; the first stage is compositional but calculates a superset of the solutions we expect from HCLP. The second stage removes precisely those solutions which are not acceptable to HCLP, but at the cost of re-introducing HCLP's non-compositional behaviour. We also discuss the compositional aspects of PCSP. The third part of this thesis presents Gocs, our system which allows the use of both the HCLP and PCSP approaches to problem relaxation and ordering. The Gocs integrated framework has HCLP and PCSP as special cases and also subsumes all of their separate advantages, when considering the characteristics of the ideal system for relaxing and resolving over-constrained problems. We present examples throughout the thesis, some of which are comparative and so may be used to substantiate our claims. Finally, we present conclusions and discuss further work.

dbProlog is a prototype system that provides a C-Prolog user access to data in an external relational database via both loose and tight coupling. To the application programmer, dbProlog is a group of six built-in Prolog predicates that effect communication between a C-Prolog process and a database management system process. Prolog application program statements may be written using the six predicates to make the interface transparent to an end-user. The system is based on a "driver" process that must be customized to the interfaced DBMS and whose primary function is the translation of requests and replies between C-Prolog and the DBMS. dbProlog supports Prolog's depth-first search on database retrievals by producing the next record when the retrieval predicate is encountered upon backtracking. dbProlog also supports multiple active database retrievals, as may be required by a Prolog rule that references two or more database retrievals, or by a recursive rule.

This thesis report describes the design and implementation of an interface between the two most common artificial intelligence languages, Lisp and Prolog. The interface is accomplished by small extensions to each language, and provides Prolog programs with the capability of invoking Lisp functions. The interface is simple yet powerful; it the supports passing of arbitrarily complex data objects, regardless of data type. The particular language implementations extended were C-Prolog [Pereira,85] and XLISP [Betz,86], both interpreters running under the Unix operating system.