Large Language Models (LLMs) have advanced Natural Language Processing (NLP) tasks but are limited in mathematical reasoning. To address this, few-shot examples are used in prompts for in-context learning. However, existing methods require annotated datasets, resulting in higher computational costs and lower quality examples. To mitigate these limitations, we propose AutoMathIC, a framework that automatically generates high-quality in-context examples to enhance LLMs’ mathematical reasoning. AutoMathIC ensures consistency across different modalities (e.g., Chain-of-Thought (CoT), code snippets, and equations) by generating and selecting mutations that improve response consistency. Evaluated on four math problem datasets, AutoMathIC outperforms six baselines, with LLM accuracy ranging from 87.0% to 99.3% for GPT-3.5 and 93.1% to 98.7% for GPT-4o-mini. It surpasses the state-of-the-art in-context example retrieval method in three of the four datasets by 0.3% to 11.8%, without relying on an annotated dataset.

Machine learning models increasingly influence decisions in high-stakes settings such as finance, law and hiring, driving the need for transparent, interpretable outcomes. However, while explainable approaches can help understand the decisions being made, they may inadvertently reveal the underlying proprietary algorithm—an undesirable outcome for many practitioners. Consequently, it is crucial to balance meaningful transparency with a form of recourse that clarifies why a decision was made and offers actionable steps following which a favorable outcome can be obtained. Counterfactual explanations offer a powerful mechanism to address this need by showing how specific input changes lead to a more favorable prediction. We propose Model-Agnostic Causally Constrained Counterfactual Generation (MC3G), a novel framework that tackles limitations in the existing counterfactual methods. First, MC3G is model-agnostic: it approximates any black-box model using an explainable rule-based surrogate model. Second, this surrogate is used to generate counterfactuals that produce a favourable outcome for the original underlying black box model. Third, MC3G refines cost computation by excluding the “effort” associated with feature changes that occur automatically due to causal dependencies. By focusing only on user-initiated changes, MC3G provides a more realistic and fair representation of the effort needed to achieve a favourable outcome. We show that MC3G delivers more interpretable and actionable counterfactual recommendations compared to existing techniques all while having a lower cost. Our findings highlight MC3G’s potential to enhance transparency, accountability, and practical utility in decision-making processes that incorporate machine-learning approaches.

Abstract Recentneuro-symbolic approaches have successfully extracted symbolic rule-sets from Convolutional Neural Network-based models to enhance interpretability. However, applying similar techniques to Vision Transformers (ViTs) remains challenging due to their lack of modular concept detectors and reliance on global self-attention mechanisms. We propose a framework for symbolic rule extraction from ViTs by introducing a sparse concept layer inspired by Sparse Autoencoders (SAEs). This linear layer operates on attention-weighted patch representations and learns a disentangled, binarized representation in which individual neurons activate for high-level visual concepts. To encourage interpretability, we apply a combination of L1 sparsity, entropy minimization, and supervised contrastive loss. These binarized concept activations are used as input to the FOLD-SE-M algorithm, which generates a rule-set in the form of a logic program. Our method achieves a better classification accuracy than the standard ViT while enabling symbolic reasoning. Crucially, the extracted rule-set is not merely post-hoc but acts as a logic-based decision layer that operates directly on the sparse concept representations. The resulting programs are concise and semantically meaningful. This work is the first to extract executable logic programs from ViTs using sparse symbolic representations, providing a step forward in interpretable and verifiable neuro-symbolic AI.

Deep learning models such as CNNs have surpassed human performance in computer vision tasks such as image classi- fication. However, despite their sophistication, these models lack interpretability which can lead to biased outcomes re- flecting existing prejudices in the data. We aim to make pre- dictions made by a CNN interpretable. Hence, we present a novel framework called NeSyFOLD to create a neurosym- bolic (NeSy) model for image classification tasks. The model is a CNN with all layers following the last convolutional layer replaced by a stratified answer set program (ASP) derived from the last layer kernels. The answer set program can be viewed as a rule-set, wherein the truth value of each pred- icate depends on the activation of the corresponding kernel in the CNN. The rule-set serves as a global explanation for the model and is interpretable. We also use our NeSyFOLD framework with a CNN that is trained using a sparse kernel learning technique called Elite BackProp (EBP). This leads to a significant reduction in rule-set size without compromising accuracy or fidelity thus improving scalability of the NeSy model and interpretability of its rule-set. Evaluation is done on datasets with varied complexity and sizes. We also pro- pose a novel algorithm for labelling the predicates in the rule- set with meaningful semantic concept(s) learnt by the CNN. We evaluate the performance of our “semantic labelling algo- rithm” to quantify the efficacy of the semantic labelling for both the NeSy model and the NeSy-EBP model.

Abstract Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools focus on automating structural aspects, they lack the ability to fully assess the semantic coherence and correctness of the assurance arguments. In prior work, we introduced the Assurance 2.0 framework that prioritizes the reasoning process, evidence utilization, and explicit delineation of counter-claims (defeaters) and counter-evidence. In this paper, we present our approach to enhancing Assurance 2.0 with semantic rule-based analysis capabilities using common-sense reasoning and answer set programming solvers, specifically s(CASP). By employing these analysis techniques, we examine the unique semantic aspects of assurance cases, such as logical consistency, adequacy, indefeasibility, etc. The application of these analyses provides both system developers and evaluators with increased confidence about the assurance case.

Abstract Recent efforts in interpreting convolutional neural networks (CNNs) focus on translating the activation of CNN filters into a stratified Answer Set Program (ASP) rule-sets. The CNN filters are known to capture high-level image concepts, thus the predicates in the rule-set are mapped to the concept that their corresponding filter represents. Hence, the rule-set exemplifies the decision-making process of the CNN w.r.t the concepts that it learns for any image classification task. These rule-sets help understand the biases in CNNs, although correcting the biases remains a challenge. We introduce a neurosymbolic framework called NeSyBiCor for bias correction in a trained CNN. Given symbolic concepts, as ASP constraints, that the CNN is biased toward, we convert the concepts to their corresponding vector representations. Then, the CNN is retrained using our novel semantic similarity loss that pushes the filters away from (or toward) learning the desired/undesired concepts. The final ASP rule-set obtained after retraining, satisfies the constraints to a high degree, thus showing the revision in the knowledge of the CNN. We demonstrate that our NeSyBiCor framework successfully corrects the biases of CNNs trained with subsets of classes from the Places dataset while sacrificing minimal accuracy and improving interpretability.

Abstract This paper proposes a new methodology for early validation of high-level requirements on cyber-physical systems with the aim of improving their quality and, thus, lowering chances of specification errors propagating into later stages of development where it is much more expensive to fix them. The paper presents a transformation of a real-world requirements specification of a medical device—the Patient-Controlled Analgesia (PCA) Pump—into an Event Calculus model that is then evaluated using Answer Set Programming and the s(CASP) system. The evaluation under s(CASP) allowed deductive as well as abductive reasoning about the specified functionality of the PCA pump on the conceptual level with minimal implementation or design dependent influences and led to fully automatically detected nuanced violations of critical safety properties. Further, the paper discusses scalability and non-termination challenges that had to be faced in the evaluation and techniques proposed to (partially) solve them. Finally, ideas for improving s(CASP) to overcome its evaluation limitations that still persist as well as to increase its expressiveness are presented.

Abstract The development of large language models (LLMs), such as GPT, has enabled the construction of several socialbots, like ChatGPT, that are receiving a lot of attention for their ability to simulate a human conversation. However, the conversation is not guided by a goal and is hard to control. In addition, because LLMs rely more on pattern recognition than deductive reasoning, they can give confusing answers and have difficulty integrating multiple topics into a cohesive response. These limitations often lead the LLM to deviate from the main topic to keep the conversation interesting. We propose AutoCompanion, a socialbot that uses an LLM model to translate natural language into predicates (and vice versa) and employs commonsense reasoning based on answer set programming (ASP) to hold a social conversation with a human. In particular, we rely on s(CASP), a goal-directed implementation of ASP as the backend. This paper presents the framework design and how an LLM is used to parse user messages and generate a response from the s(CASP) engine output. To validate our proposal, we describe (real) conversations in which the chatbot’s goal is to keep the user entertained by talking about movies and books, and s(CASP) ensures (i) correctness of answers, (ii) coherence (and precision) during the conversation—which it dynamically regulates to achieve its specific purpose—and (iii) no deviation from the main topic.

Abstract We present Locksynth, a tool that automatically derives synchronization needed for destructive updates to concurrent data structures that involve a constant number of shared heap memory write operations. Locksynth serves as the implementation of our prior work on deriving abstract synchronization code. Designing concurrent data structures involves inferring correct synchronization code starting with a prior understanding of the sequential data structure’s operations. Further, an understanding of shared memory model and the synchronization primitives is also required. The reasoning involved transforming a sequential data structure into its concurrent version can be performed using Answer Set Programming, and we mechanized our approach in previous work. The reasoning involves deduction and abduction that can be succinctly modeled in ASP. We assume that the abstract sequential code of the data structure’s operations is provided, alongside axioms that describe concurrent behavior. This information is used to automatically derive concurrent code for that data structure, such as dictionary operations for linked lists and binary search trees that involve a constant number of destructive update operations. We also are able to infer the correct set of locks (but not code synthesis) for external height-balanced binary search trees that involve left/right tree rotations. Locksynth performs the analyses required to infer correct sets of locks and as a final step, also derives the C++ synchronization code for the synthesized data structures. We also provide a performance analysis of the C++ code synthesized by Locksynth with the hand-crafted versions available from the Synchrobench microbenchmark suite. To the best of our knowledge, our tool is the first to employ ASP as a backend reasoner to perform concurrent data structure synthesis.

In the analogy-based learning method we map a concept that is being learned to a well-understood concept. An analogy is mainly useful when learners lack prior knowledge of the topic being learned. Software Engineering (SE) is a subject whose concepts tend to be highly abstract and therefore difficult for undergraduate students to understand. Analogy-based instruction can greatly reduce a student’s burden of learning these abstract SE concepts. Role of Analogy in teaching SE topics has not been adequately explored. In this paper we discuss analogy-based instruction in software engineering and its advantages. Over the last decade we have developed analogies for many complex SE concepts and extensively used them in the classroom at our institution. We discuss these concepts and corresponding analogies and as an illustration discuss one of them in detail. We also present the evaluation of our analogy-based instruction method. Our results indicate that the analogies we have developed are quite effective in improving student learning outcomes.

Abstract Automated commonsense reasoning (CR) is essential for building human-like AI systems featuring, for example, explainable AI. Event calculus (EC) is a family of formalisms that model CR with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains (e.g. time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query-driven, top-down execution model for Predicate Answer Set Programming with Constraints, to model and reason using EC. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks in domains featuring constraints involving both dense time and dense fluents.

Abstract Building Information Modeling (BIM) produces three-dimensional object-oriented models of buildings combining the geometrical information with a wide range of properties about materials, products, safety, to name just a few. BIM is slowly but inevitably revolutionizing the architecture, engineering, and construction industry. Buildings need to be compliant with regulations about stability, safety, and environmental impact. Manual compliance checking is tedious and error-prone, and amending flaws discovered only at construction time causes huge additional costs and delays. Several tools can check BIM models for conformance with rules/guidelines. For example, Singapore’s CORENET e-Submission System checks fire safety. But since the current BIM exchange format only contains basic information about building objects, a separate, ad-hoc model pre-processing is required to determine, for example, evacuation routes. Moreover, they face difficulties in adapting existing built-in rules and/or adding new ones (to cater for building regulations, that can vary not only among countries but also among parts of the same city), if at all possible. We propose the use of logic-based executable formalisms (CLP and Constraint ASP) to couple BIM models with advanced knowledge representation and reasoning capabilities. Previous experience shows that such formalisms can be used to uniformly capture and reason with knowledge (including ambiguity) in a large variety of domains. Additionally, incorporating checking within design tools makes it possible to ensure that models are rule-compliant at every step. This also prevents erroneous designs from having to be (partially) redone, which is also costly and burdensome. To validate our proposal, we implemented a preliminary reasoner under CLP(Q/R) and ASP with constraints and evaluated it with several BIM models.

Abstract Multi-core and highly connected architectures have become ubiquitous, and this has brought renewed interest in language-based approaches to the exploitation of parallelism. Since its inception, logic programming has been recognized as a programming paradigm with great potential for automated exploitation of parallelism. The comprehensive survey of the first twenty years of research in parallel logic programming, published in 2001, has served since as a fundamental reference to researchers and developers. The contents are quite valid today, but at the same time the field has continued evolving at a fast pace in the years that have followed. Many of these achievements and ongoing research have been driven by the rapid pace of technological innovation, that has led to advances such as very large clusters, the wide diffusion of multi-core processors, the game-changing role of general-purpose graphic processing units, and the ubiquitous adoption of cloud computing. This has been paralleled by significant advances within logic programming, such as tabling, more powerful static analysis and verification, the rapid growth of Answer Set Programming, and in general, more mature implementations and systems. This survey provides a review of the research in parallel logic programming covering the period since 2001, thus providing a natural continuation of the previous survey. In order to keep the survey self-contained, it restricts its attention to parallelization of the major logic programming languages (Prolog, Datalog, Answer Set Programming) and with an emphasis on automated parallelization and preservation of the sequential observable semantics of such languages. The goal of the survey is to serve not only as a reference for researchers and developers of logic programming systems but also as engaging reading for anyone interested in logic and as a useful source for researchers in parallel systems outside logic programming.

Abstract An approach based on answer set programming (ASP) is proposed in this paper for representing knowledge generated from natural language texts. Knowledge in a text is modeled using a Neo Davidsonian-like formalism, which is then represented as an answer set program. Relevant commonsense knowledge is additionally imported from resources such as WordNet and represented in ASP. The resulting knowledge-base can then be used to perform reasoning with the help of an ASP system. This approach can facilitate many natural language tasks such as automated question answering, text summarization, and automated question generation. ASP-based representation of techniques such as default reasoning, hierarchical knowledge organization, preferences over defaults, etc., are used to model commonsense reasoning methods required to accomplish these tasks. In this paper, we describe the CASPR system that we have developed to automate the task of answering natural language questions given English text. CASPR can be regarded as a system that answers questions by “understanding” the text and has been tested on the SQuAD data set, with promising results.

Abstract FOLD-RM is an automated inductive learning algorithm for learning default rules for mixed (numerical and categorical) data. It generates an (explainable) answer set programming (ASP) rule set for multi-category classification tasks while maintaining efficiency and scalability. The FOLD-RM algorithm is competitive in performance with the widely used, state-of-the-art algorithms such as XGBoost and multi-layer perceptrons, however, unlike these algorithms, the FOLD-RM algorithm produces an explainable model. FOLD-RM outperforms XGBoost on some datasets, particularly large ones. FOLD-RM also provides human-friendly explanations for predictions.

Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) research. An ideal NLU system should process a language in a way that is not exclusive to a single task or a dataset. Keeping this in mind, we have introduced a novel knowledge driven semantic representation approach for English text. By leveraging the VerbNet lexicon, we are able to map syntax tree of the text to its commonsense meaning represented using basic knowledge primitives. The general purpose knowledge represented from our approach can be used to build any reasoning based NLU system that can also provide justification. We applied this approach to construct two NLU applications that we present here: SQuARE (Semantic-based Question Answering and Reasoning Engine) and StaCACK (Stateful Conversational Agent using Commonsense Knowledge). Both these systems work by ``truly understanding'' the natural language text they process and both provide natural language explanations for their responses while maintaining high accuracy.

Abstract We focus on the problem of inducing logic programs that explain models learned by the support vector machine (SVM) algorithm. The top-down sequential covering inductive logic programming (ILP) algorithms (e.g., FOIL) apply hill-climbing search using heuristics from information theory. A major issue with this class of algorithms is getting stuck in local optima. In our new approach, however, the data-dependent hill-climbing search is replaced with a model-dependent search where a globally optimal SVM model is trained first, then the algorithm looks into support vectors as the most influential data points in the model, and induces a clause that would cover the support vector and points that are most similar to that support vector. Instead of defining a fixed hypothesis search space, our algorithm makes use of SHAP, an example-specific interpreter in explainable AI, to determine a relevant set of features. This approach yields an algorithm that captures the SVM model’s underlying logic and outperforms other ILP algorithms in terms of the number of induced clauses and classification evaluation metrics.

We present a heuristic based algorithm to induce nonmonotonic logic programs that will explain the behavior of XGBoost trained classifiers. We use the technique based on the LIME approach to locally select the most important features contributing to the classification decision. Then, in order to explain the model’s global behavior, we propose the LIME-FOLD algorithm —a heuristic-based inductive logic programming (ILP) algorithm capable of learning nonmonotonic logic programs—that we apply to a transformed dataset produced by LIME. Our proposed approach is agnostic to the choice of the ILP algorithm. Our experiments with UCI standard benchmarks suggest a significant improvement in terms of classification evaluation metrics. Meanwhile, the number of induced rules dramatically decreases compared to ALEPH, a state-of-the-art ILP system.

Abstract Extending ASP with constraints (CASP) enhances its expressiveness and performance. This extension is not straightforward as the grounding phase, present in most ASP systems, removes variables and the links among them, and also causes a combinatorial explosion in the size of the program. Several methods to overcome this issue have been devised: restricting the constraint domains (e.g., discrete instead of dense), or the type (or number) of models that can be returned. In this paper we propose to incorporate constraints into s(ASP), a goal-directed, top-down execution model which implements ASP while retaining logical variables both during execution and in the answer sets. The resulting model, s(CASP), can constrain variables that, as in CLP, are kept during the execution and in the answer sets. s(CASP) inherits and generalizes the execution model of s(ASP) and is parametric w.r.t. the constraint solver. We describe this novel execution model and show through several examples the enhanced expressiveness of s(CASP) w.r.t. ASP, CLP, and other CASP systems. We also report improved performance w.r.t. other very mature, highly optimized ASP systems in some benchmarks.

Abstract Management of chronic diseases, such as heart failure, is a major public health problem. A standard approach to managing chronic diseases by medical community is to have a committee of experts develop guidelines that all physicians should follow. Due to their complexity, these guidelines are difficult to implement and are adopted slowly by the medical community at large. We have developed a physician advisory system that codes the entire set of clinical practice guidelines for managing heart failure using answer set programming. In this paper, we show how abductive reasoning can be deployed to find missing symptoms and conditions that the patient must exhibit in order for a treatment prescribed by a physician to work effectively. Thus, if a physician does not make an appropriate recommendation or makes a non-adherent recommendation, our system will advise the physician about symptoms and conditions that must be in effect for that recommendation to apply. It is under consideration for acceptance in TPLP.

Abstract In inductive learning of a broad concept, an algorithm should be able to distinguish concept examples from exceptions and noisy data. An approach through recursively finding patterns in exceptions turns out to correspond to the problem of learning default theories. Default logic is what humans employ in common-sense reasoning. Therefore, learned default theories are better understood by humans. In this paper, we present new algorithms to learn default theories in the form of non-monotonic logic programs. Experiments reported in this paper show that our algorithms are a significant improvement over traditional approaches based on inductive logic programming. Under consideration for acceptance in TPLP.

Abstract Management of chronic diseases such as chronic heart failure (CHF) is a major problem in health care. A standard approach followed by the medical community is to have a committee of experts develop guidelines that all physicians should follow. These guidelines typically consist of a series of complex rules that make recommendations based on a patient's information. Due to their complexity, often the guidelines are ignored or not complied with at all. It is not even clear whether it is humanly possible to follow these guidelines due to their length and complexity. For instance, for CHF, the guidelines run nearly eighty pages. In this paper we describe a physician-advisory system for CHF management that codes the entire set of clinical practice guidelines for CHF using answer set programming (ASP). Our approach is based on developing reasoning templates, that we call knowledge patterns, and using them to systemically code the clinical guidelines for CHF as ASP rules. Use of the knowledge patterns greatly facilitates the development of our system. Given a patient's medical information, our system generates a recommendation for treatment just as a human physician would, using the guidelines. Our system works even in the presence of incomplete information.

Abstract In answer set programming, inconsistencies arise when the constraints placed on a program become unsatisfiable. In this paper, we introduce a technique fordynamic consistency checkingfor our goal-directed method for computing answer sets, under which only those constraints deemed relevant to the partial answer set are tested, allowing inconsistent knowledgebases to be successfully queried. However, the algorithm guarantees that, if a program has at least one consistent answer set, any partial answer set returned will be a subset of some consistent answer set.

We have developed a real-time sleep apnea monitoring system called “Apnea MedAssist II”. This has three independent sensors: ECG, SpO2 and Breath sensor. These sensors are connected to a smartphone via Bluetooth. The signal processing of the sensor signals and automated classification of a sleep epoch as an apnea event or a non-apnea event are done in a smart phone. The soft ware for signal processing and automated classification can be imported to an Android OS based smart phones as an `app' that we have developed. The system has accuracy well over 97% when tested on Physionet database. The system is being readied for limited patient trial.

Answer Set Programming (ASP) represents an elegant way of introducing non-monotonic reasoning into logic programming. ASP has gained popularity due to its applications to planning, default reasoning and other areas of AI. However, none of the approaches and current implementations for ASP are goal-directed. In this paper we present a technique based coinduction that can be employed to design SLD resolution-style, goal-directed methods for executing answer set programs. We also discuss advantages and applications of such goal-directed execution of answer set programs, and report results from our implementation.

Service-oriented computing (SOC) has emerged as the eminent market environment for sharing and reusing service-centric capabilities. The underpinning for an organization's use of SOC techniques is the ability to discover and compose Web services. Although industry approaches to composition have a strong notion of business processes, these approaches largely use syntactic descriptions. As such composition is limited since the true functionality of ambiguous service operations cannot be inferred. Alternatively, academia uses semantic approaches to disambiguate services, but, at the same time, most of these approaches neglect the process rigor needed for complex compositions. In this paper we present a generalized semantics-based technique for automatic service composition that combines the rigor of process-oriented composition with the descriptiveness of semantics. Our generalized approach extends the common practice of linearly linked services by introducing the use of a conditional directed acyclic graph (DAG) where complex interactions, containing control flow, information flow and pre/post conditions, are effectively represented. Furthermore, the composition can be represented semantically as OWL-S documents. Our contributions are applied for automatic workflow generation in context of the currently important bioinformatics domain.

Abstract In the dynamic programming paradigm the value of an optimal solution is recursively defined in terms of optimal solutions to subproblems. Such dynamic programming definitions can be tricky and error‐prone to specify. This paper presents an elegant method based on tabled logic programming (TLP) that simplifies the specification of such dynamic programming solutions. Our method introduces a new mode declaration for tabled predicates. The arguments of each tabled predicate are divided into indexed and non‐indexed arguments so that tabled predicates can be regarded as functions: indexed arguments represent input values and non‐indexed arguments represent output values. The non‐indexed arguments in a tabled predicate can be further declared to be aggregated, for example, the minimum, so that while generating answers, the global table will dynamically maintain the smallest value for that argument. This mode‐declaration scheme, coupled with recursion, provides an easy‐to‐use method for dynamic programming: there is no need to define the value of an optimal solution recursively, as the definition of a general solution suffices. The optimal value as well as its corresponding concrete solution can be derived implicitly and automatically using tabled logic programming systems. Our experimental results show that mode declarations improve performance in solving dynamic programming problems on TLP systems. Copyright © 2007 John Wiley & Sons, Ltd.

Service-oriented computing is gaining wider acceptance. For Web services to become practical, an infrastructure needs to be supported that allows users and applications to discover, deploy, compose and synthesize services automatically. For this automation to be effective, formal semantic descriptions of Web services should be available. In this paper we formally define the Web service discovery and composition problem and present an approach for automatic service discovery and composition based on semantic description of Web services. We also report on an implementation of a semantics-based automated service discovery and composition engine that we have developed. This engine employs a multi-step narrowing algorithm and is efficiently implemented using the constraint logic programming technology. The salient features of our engine are its scalability, i.e., its ability to handle very large service repositories, and its extremely efficient processing times for discovery and composition queries. We evaluate our engine for automated discovery and composition on repositories of different sizes and present the results.

Abstract This paper describes the development of thePALSsystem, an implementation of Prolog capable of efficiently exploiting or-parallelism ondistributed-memoryplatforms—specifically Beowulf clusters. PALS makes use of a novel technique, calledincremental stack-splitting. The technique proposed builds on the stack-splitting approach, previously described by the authors and experimentally validated on shared-memory systems, which in turn is an evolution of the stack-copying method used in a variety of parallel logic and constraint systems—e.g., MUSE, YAP, and Penny. The PALS system is the first distributed or-parallel implementation of Prolog based on the stack-splitting method ever realized. The results presented confirm the superiority of this method as a simple yet effective technique to transition from shared-memory to distributed-memory systems. PALS extends stack-splitting by combining it with incremental copying; the paper provides a description of the implementation of PALS, including details of how distributed scheduling is handled. We also investigate methodologies to effectively support order-sensitive predicates (e.g., side-effects) in the context of the stack-splitting scheme. Experimental results obtained from running PALS on both Shared Memory and Beowulf systems are presented and analyzed.

The VoxBoox system makes digital books accessible to visually impaired individuals via audio and voice. It automatically translates a book published in HTML to VoiceXML, and then further enhances this VoiceXML rendering of the book to enable listener-controlled dynamic aural navigation. The VoxBoox system has the following salient features: (i) it leverages existing infrastructure since the book that is to be made accessible need only be published digitally using HTML on the visual Web, (ii) it is based on accepted Web standards of HTML and VoiceXML and thus books can be made accessible inexpensively, and (iii) it is user-centered in that the listener (the user) has complete control over (aural) navigation of the book. In this paper, we present details of the technologies that make the VoxBoox system possible, as well as the details of the system itself. A prototype of the VoxBoox system is operational.

In a short period the Web has become an important part of our lives. However, the full potential of the Web is still not realized. Two recent developments - Web services and the semantic Web - are steps in the direction of utilizing the full potential of the Web. Web services allow applications to utilize the Web for automatically extracting (and updating) information while the semantic Web enterprise promises to provide the infrastructure that allows intelligent Web services to be rapidly created and deployed. However, with this comes the task of transforming the traditional Web-based systems to Web-services over the semantic Web. In this paper, we demonstrate how an existing successful Web-based system for providing help to first responders of chemically hazardous emergencies (called E-plan) can be converted into a Web-services based model using the semantic Web and intelligent reasoning technologies. Our efforts can be regarded as a case study in converting monolithic Web-based applications to a more agile, rapidly deployable intelligent Web-services model.

To fully utilize Web-services, users and applications should be able to discover, deploy, compose and synthesize services automatically. This automation can take place only if a formal semantic description of the Web-services is available. In this paper we present a markup language called USDL (Universal Service Description Language), for formally describing the semantics of Web-services.

Traditional constraint programming specifies an optimization problem by using a set of constraints and minimizing (or maximizing) objective functions. Unfortunately, general optimization problems may involve compound objectives whose optima are difficult to be represented by a simple minimization (or maximization). Even worse, for many applications, especially those defined over structural domains, it is difficult to specify any objective functions. In this paper we presents a declarative method for specifying generalized optimization problems based on comparison and selection among alternative solutions. The method introduces a formal predicate mode declaration for designating certain predicates as optimization predicates, and uses preference rules for stating the criteria for determining their optimal solutions. We illustrate their uses with two representative examples: one is matrix-chain multiplication from dynamic programming, and the other is ambiguity resolution for recursively-defined grammars. This paper also addresses how to extend a tabled Prolog system with preferences. The execution of logic programs with preferences is achieved in two steps. First, an automatic transformation is applied to embed the preferences into the problem specification to form an executable program. Second, the new program is then evaluated using tabled resolution, while the mode declaration provides a selection mechanism among the alternative solutions. We show that the transformation scheme preserves the semantics for each optimization predicate. Experimental results are shown to indicate that preferences provide a declarative approach without sacrificing efficiency.

We describe the UMA system, a system developed under a multi-institution collaboration for making mathematics universally accessible. The UMA system includes translators that freely inter-convert mathematical documents transcribed in formats used by unsighted individual (Nemeth, Marburg) to those used by sighted individuals (LaTeX, Math-ML, OpenMath) and vice versa. The UMA system also includes notation-independent tools for aural navigation of mathematics. In this paper, we give an overview of the UMA system and the techniques used for realizing it.

We consider the problem of automatically checking if coding standards have been followed in the development of embedded applications. The problem arises from practical considerations because DSP chip manufacturers (in our case Texas Instruments) want various third party software developers to adhere to a certain coding standard to facilitate system integration during application development. Checking for compliance with coding standards, in general, is undecidable. Moreover, only machine code of the system components is available since for proprietary reasons vendors of various components do not want to share their source code. In this paper, we describe an approach based on static analysis of embedded assembly code to check for compliance with such coding standards. This static analysis rests on an abstract interpretation framework. We illustrate our approach by showing how we statically analyze the presence of hard-coded pointer variables in embedded assembly code. Hard coded pointer variables are those that are assigned a fixed memory address by the programmer instead of being assigned a value via proper operations in the source language (e.g., malloc/calloc/realloc and & operator in C). Our analyzer takes object code as input, disassembles it, builds the flow-graph, and statically analyzes the flow-graph for the presence of dereferenced pointers that are hard coded. The analyzer is currently being extended to check for compliance with other rules adopted by TI as part of its coding standards.

In this paper, we provide a progress report on the development of technology to support the non-visual navigation of complex HTML and XML structures.

Incremental stack-copying is a technique which has been successfully used to support efficient parallel execution of a variety of search-based Al systems-e.g., logic-based and constraint-based systems. The idea of incremental stack-copying is to only copy the difference between the data areas of two agents, instead of copying them entirely, when distributing parallel work. In order to further reduce the communication during stack-copying and make its implementation efficient on message-passing platforms, a new technique, called stack-splitting, has recently been proposed. In this paper, we describe a scheme to effectively combine stack-splitting with incremental stack copying, to achieve superior parallel performance in a non-shared memory environment. We also describe a scheduling scheme for this incremental stack-splitting strategy. These techniques are currently being implemented in the PALS system-a parallel constraint logic programming system.

Abstract Naive parallel implementation of non‐deterministic systems (such as a theorem proving system) and languages (such as logic, constraint, or concurrent constraint languages) can result in poor performance. We present three optimization schemas, based onflattening of the computation tree,procrastination of overheads, andsequentialization of computationsthat can be systematically applied to parallel implementations of non‐deterministic systems/languages to reduce the parallel overhead and to obtain improved efficiency of parallel execution. The effectiveness of these schemas is illustrated by applying them to the ACE parallel logic programming system. The performance data presented show that considerable improvement in execution efficiency can be achieved. Copyright © 2001 John Wiley & Sons, Ltd.

Since the early days of logic programming, researchers in the field realized the potential for exploitation of parallelism present in the execution of logic programs. Their high-level nature, the presence of nondeterminism, and their referential transparency, among other characteristics, make logic programs interesting candidates for obtaining speedups through parallel execution. At the same time, the fact that the typical applications of logic programming frequently involve irregular computations, make heavy use of dynamic data structures with logical variables, and involve search and speculation, makes the techniques used in the corresponding parallelizing compilers and run-time systems potentially interesting even outside the field. The objective of this article is to provide a comprehensive survey of the issues arising in parallel execution of logic programming languages along with the most relevant approaches explored to date in the field. Focus is mostly given to the challenges emerging from the parallel execution of Prolog programs. The article describes the major techniques used for shared memory implementation of Or-parallelism, And-parallelism, and combinations of the two. We also explore some related issues, such as memory management, compile-time analysis, and execution visualization.

In this paper, we present an implementation model which efficiently supports backtracking in an independent and-parallel nondeterministic system. The problem is tackled in the context of logic programming, although the solution proposed is sufficiently general to be easily extended to different nondeterministic systems, such as constraint programming systems. The complexity of the problem is demonstrated by the fact that most existing and-parallel systems either do not support backtracking over and-parallel calls or simply avoid analyzing the performance of their systems in the presence of nondeterministic benchmarks. The implementation model we present is an extension of the backtracking scheme developed by Hermenegildo and Nasr (1986) and relies on a novel memory organization scheme and on the use of various optimizations to reduce communication and overhead. The solution developed has been implemented in the ACE Parallel Prolog system. The performance of the system is analyzed on a variety of benchmarks. The results obtained are remarkable: speedups achieved during forward execution are not lost in heavy backtracking activities and, frequently, super-linear speedups are obtained thanks to a semi-intelligent backtracking scheme.

We present a general framework for navigating complex structures - specifically, tables, frames, and forms?found in web-pages. Our framework is based on an (automatically or manually created) program written in a domain specific language that captures the semantic structure of the table/frame/form as well as specifies the strategy to be used for navigating it. We describe our general framework and the domain specific language we have designed.

We study the problem of exploiting parallelism from search-based AI systems on distributed machines. We propose stack-splitting, a technique for implementing or-parallelism, which when coupled with appropriate scheduling strategies leads to: (i) reduced communication during distributed execution; and, (ii) distribution of larger grain- sized work to processors. The modified technique can also be implemented on shared memory machines and should be quite competitive with existing methods. Indeed, an implementation has been carried out on shared memory machines, and the results are reported here.

One of the greatest challenges to the visually impaired student in science and mathematics disciplines is the reading and writing of complex mathematical equations or have convenient access to information based tools such as the world wide web. In research currently underway at New Mexico State University, tools are being built using logic programming to facilitate access to complex information in a variety of formats. On top of the logic based tools, new interfaces are being designed to permit more convenient access to information by our visually impaired students.

We show how parallelizing compilers can be automatically derived from denotational definitions of programming languages. In our approach, the denotational definition is expressed using definite clause grammars (syntax specification) and Horn Logic or Constraint Logic (semantic specification). The conditions for executing two or more statements in parallel (e.g. GCD test, Banerjee test, or exact test) are included as part of the parallel denotational semantics of the language. Solutions of Diophantine equations, needed for parallelizing DO loops, can be expressed in constraint logic as well, and are thus easily incorporated in our denotational framework. This parallel denotational specification of the language is executable, and thus automatically yields a parallel interpreter. This interpreter can be partially evaluated with respect to a given program to automatically obtain (provably correct) parallel compiled code. In addition, the various syntactic and semantic restructuring transformations that have been proposed to expose more parallelism in sequential programs can also be expressed in our denotational framework.

We consider the problem of efficiently supporting backtracking in independent and-parallel non-deterministic systems. We consider this problem in the context of logic programming, although the solution proposed is sufficiently general to be applicable to any non-deterministic language or system. Our model employs various optimizations, as well as a novel memory organization scheme in which processors are allowed to traverse each others' stacks to achieve this efficiency. The solution developed has been implemented in the ACE Prolog system. The performance of the system is analyzed on a variety of non-deterministic benchmarks.

The development of the World Wide Web (WWW) has been considerably delayed due to the excessive complexity of developing advanced and intelligent applications for the Internet. An average application may require the use of different languages, an in-depth understanding of various communication protocols and low-level communication mechanisms, etc. We propose a logic programming system, called W-ACE, extended with various features to support natural and efficient development of Internet tools. The nature of the constructs introduced makes it particularly suitable to support intelligent Internet applications (knowledge-based systems, agents, etc.). W-ACE covers various issues in supporting knowledge-based handling of the World Wide Web, allowing structured and constraint-based management of WWW information, passive and active views of WWW, as well as a powerful support for concurrent applications. Various examples of complex intelligent applications are presented, to underline the simplicity and the power of the proposed ideas.

We develop a general constraint logic programming (CLP) based framework for specification and verification of real time systems. Our framework is based on the notion of timed automata that have traditionally been used for specifying real time systems. In our framework, a user models the ordering of real time events as the grammar of a language accepted by a timed automata, the real time constraints on these events are then captured as denotations of the grammar productions specified by the user. The grammar can be specified as a Definite Clause Grammar (DCG), while the denotations can be specified in constraint logic. The resulting specification can hence be regarded as a constraint logic program (CLP), and is executable. Many interesting properties of the real time system can be verified by posing appropriate queries to this CLP program. A major advantage of our approach is that it is constructive in nature, i.e., it can be used for computing the conditions under which a property will hold for a given real time system. Our framework also suggests new types of formalisms that we call constraint automata and timed push down automata.

We discuss fundamental limitations of or-parallel execution models of nondeterministic programming languages. Or-parallelism corresponds to the execution of different nondeterministic computational paths in parallel. A natural way to represent the state of (parallel) execution of a nondeterministic program is by means of an or-parallel tree. We identify three important criteria that underlie the design of or-parallel implementations based on the or-parallel tree: constant-time access to variables, constant-time task creation, and constant-time task switching, where the term constant-time means that the time for these operations is independent of the number of nodes in the or-parallel tree, as well as the size of each node. We prove that all three criteria cannot be simultaneously satisfied by any or-parallel execution model based on a finite number of processors but unbounded memory. We discuss in detail the application of our result to the class of logic programming languages and show how our result can serve as a useful way to categorize the various or-parallel methods proposed in this field. We also discuss the suitability of different or-parallel implemenation strategies for different parallel architectures.

EqL, a general-purpose language that combines the capabilities of functional and logic programming languages, is described. A program in EqL consists of a collection of conditional, pattern-directed rules, where the conditions are expressed as a conjunction of equations, and the patterns are terms built up of data-constructors and basic values. The computational paradigm in EqL is equation solving. Examples illustrating the major features of the language, nondeterminism, deferred evaluation of primitives, and logical variables are presented. The aspects of a sequential implementation for EqL, such as compile-time flattening of equations, run-time equation-delaying, and last-equation optimization, are also described.>

A universal test set for CMOS circuits is demonstrated that can be derived from the functional description of the circuit alone. It is shown that for a restricted class of CMOS circuits, the gate-level universal test set (UTS/sub g/) consisting of maximal false vectors and minimal true vectors can sensitize every detectable stuck-open fault in the circuit. A universal initialization set (UIS) is defined which can also be derived from just the functional description, and which contains initialization vectors for each of the test vectors. This set consists of maximal true vectors and minimal false vectors. It is shown that a test set on UTS/sub g/ and UIS can be guaranteed to detect every detectable stuck-open fault in both redundant and irredundant CMOS implementation of the function, even in the presence of arbitrary delays and timing-skews. The size of the test set is also investigated.>