Program synthesis is an active research field in academia, national labs, and industry. Yet, work directly applicable to scientific computing, while having some impressive successes, has been limited. This report reviews the relevant areas of program synthesis work for scientific computing, discusses successes to date, and outlines opportunities for future work. This report is the result of the Workshop on Program Synthesis for Scientific Computing was held virtually on August 4-5 2020 (https://prog-synth-science.github.io/2020/).

To increase automation in proof assistants and other verification tools based on higher-order formalisms, we propose to generalize superposition to an extensional, polymorphic, clausal version of higher-order logic (also called simple type theory). Our ambition is to achieve a graceful extension, which coincides with standard superposition on first-order problems and smoothly scales up to arbitrary higher-order problems. Bentkamp, Blanchette, Cruanes, and Waldmann [12] designed a family of superpositionlike calculi for a λ-free clausal fragment of higher-order logic, with currying and applied variables. We adapt their extensional nonpurifying calculus to support λ-terms (Sect.

Sequences and time-series often arise in robot tasks, e.g., in activity recognition and imitation learning. In recent years, deep neural networks (DNNs) have emerged as an effective data-driven methodology for processing sequences given sufficient training data and compute resources. However, when data is limited, simpler models such as logic/rule-based methods work surprisingly well, especially when relevant prior knowledge is applied in their construction. However, unlike DNNs, these "structured" models can be difficult to extend, and do not work well with raw unstructured data. In this work, we seek to learn flexible DNNs, yet leverage prior temporal knowledge when available. Our approach is to embed symbolic knowledge expressed as linear temporal logic (LTL) and use these embeddings to guide the training of deep models. Specifically, we construct semantic-based embeddings of automata generated from LTL formula via a Graph Neural Network. Experiments show that these learnt embeddings can lead to improvements in downstream robot tasks such as sequential action recognition and imitation learning.

In this paper, we deal with a calculus system SLCD (Syllogistic Logic with Carroll Diagrams), which gives a formal approach to logical reasoning with diagrams, for representations of the fundamental Aristotelian categorical propositions and show that they are closed under the syllogistic criterion of inference which is the deletion of middle term. Therefore, it is implemented to let the formalism comprise synchronically bilateral and trilateral diagrammatical appearance and a naive algorithmic nature. And also, there is no need specific knowledge or exclusive ability to understand as well as to use it. Consequently, we give an effective algorithm used to determine whether a syllogistic reasoning valid or not by using SLCD.

The paper analyzes the parameterized complexity of evaluating Ontology Mediated Queries (OMQs) based on Guarded TGDs (GTGDs) and Unions of Conjunctive Queries (UCQs), in the setting where relational symbols might have unbounded arity and where the parameter is the size of the OMQ. It establishes exact criteria for fixed-parameter tractability (fpt) evaluation of recursively enumerable classes of such OMQs (under the widely held Exponential Time Hypothesis). One of the main technical tools introduced in the paper is an fpt-reduction from deciding parameterized uniform CSPs to parameterized OMQ evaluation. A fundamental feature of the reduction is preservation of measures which are known to be essential for classifying classes of parameterized uniform CSPs: submodular width (according to the well known result of Marx for unbounded-arity schemas) and treewidth (according to the well known result of Grohe for bounded-arity schemas). As such, the reduction can be employed to obtain hardness results for evaluation of classes of parameterized OMQs both in the unbounded and in the bounded arity case. Previously, in the case of bounded arity schemas, this has been tackled using a technique requiring full introspection into the construction employed by Grohe.

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.

The field of Artificial Intelligence (AI) has undoubtedly received significant attention in recent years. AI is being adopted to provide solutions to problems in fields such as medicine, engineering, education, government and several other domains. In order to analyze the state of the art of research in the field of AI, we present a systematic literature review focusing on the Evolution of AI programming languages. We followed the systematic literature review method by searching relevant databases like SCOPUS, IEEE Xplore and Google Scholar. EndNote reference manager was used to catalog the relevant extracted papers. Our search returned a total of 6565 documents, whereof 69 studies were retained. Of the 69 retained studies, 15 documents discussed LISP programming language, another 34 discussed PROLOG programming language, the remaining 20 documents were spread between Logic and Object Oriented Programming (LOOP), ARCHLOG, Epistemic Ontology Language with Constraints (EOLC), Python, C++, ADA and JAVA programming languages. This review provides information on the year of implementation, development team, capabilities, limitations and applications of each of the AI programming languages discussed. The information in this review could guide practitioners and researchers in AI to make the right choice of languages to implement their novel AI methods.

The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.

For a d-ary Boolean function Φ: {0, 1}d → {0, 1} and an assignment to its variables x = (x1, x2, . . . , xd) we consider the problem of finding those subsets of the variables that are sufficient to determine the function value with a given probability δ. This is motivated by the task of interpreting predictions of binary classifiers described as Boolean circuits, which can be seen as special cases of neural networks. We show that the problem of deciding whether such subsets of relevant variables of limited size k ≤ d exist is complete for the complexity class NPPP and thus, generally, unfeasible to solve. We then introduce a variant, in which it suffices to check whether a subset determines the function value with probability at least δ or at most δ − γ for 0 < γ < δ. This promise of a probability gap reduces the complexity to the class NPBPP. Finally, we show that finding the minimal set of relevant variables cannot be reasonably approximated, i.e. with an approximation factor d1−α for α > 0, by a polynomial time algorithm unless P = NP. This holds even with the promise of a probability gap.

The mathematics of quantum mechanics has been viewed and analyzed from a huge variety of different perspectives, each shedding light on different subtleties of its underlying structure and its connection to our everyday reality. Here we add an additional thread to this conceptual polyphony, demonstrating a close connection between fuzzy paraconsistent logic and quantum probabilities. This connection suggests new variations on existing interpretations of quantum reality and measurement. It also provides some tantalizing connections between the probabilistic and fuzzy logic used in modern AI systems and quantum probabilistic reasoning, which may have implications for quantum-computing implementations of logical inference based AI. The ideas here arose as a spinoff from the work reported in [Goe21], which uses a variety of paraconsistent intuitionistic logic called Constructible Duality (CD) Logic as a means for giving a rigorous logic foundation to the PLN (Probabilistic Logic Networks) logic [GIGH08] that has been used in the OpenCog AI project [GPG13a, GPG13b] for well over a decade now.