We will investigate proof-theoretic and linguistic aspects of first-order linear logic. We will show that adding partial order constraints in such a way that each sequent defines a unique linear order on the antecedent formulas of a sequent allows us to define many useful logical operators. In addition, the partial order constraints improve the efficiency of proof search.
Residuation theory concerns the study of partially ordered algebraic structures, most often monoids, equipped with a weak inverse for the monoidal operator. One of its area of application has been constraint programming, whose key requirement is the presence of an aggregator operator for combining preferences. Given a residuated monoid of preferences, the paper first shows how to build a new residuated monoid of (possibly infinite) tuples, which is based on the lexicographic order. Second, it introduces a variant of an approximation technique (known as Mini-bucket) that exploits the presence o…
In this paper, we introduce $\textit{partial}$ dependency modality $\mathcal{D}$ into epistemic logic so as to reason about $\textit{partial}$ dependency relationship in Kripke models. The resulted dependence epistemic logic possesses decent expressivity and beautiful properties. Several interesting examples are provided, which highlight this logic's practical usage. The logic's bisimulation is then discussed, and we give a sound and strongly complete axiomatization for a sub-language of the logic.
The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established.
I consider the following generic scenario: an abstract model M of some 'real' system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in some logical language. This scenario has at least two essentially different interpretations, leading to two, essentially different, formal logical and algorithmic problems: "Model Synthesis from Partial Models", where some 'admissible' extension of M to a full model must satisfy the specification, and "Model Checking of Partial Models", where all 'admissible' extens…
We present an illative system I_s of classical higher-order logic with subtyping and basic inductive types. The system I_s allows for direct definitions of partial and general recursive functions, and provides means for handling functions whose termination has not been proven. We give examples of how properties of some recursive functions may be established in our system. In a technical appendix to the paper we prove consistency of I_s. The proof is by model construction. We then use this construction to show conservativity of I_s over classical first-order logic. Conservativity over higher-or…
Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed-point logic. Inclusion logic is not axiomatizable in full, but its first-order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first-order consequences in inclusion logic.
Defeasible rules are used in providing computable representations of legal documents and, more recently, have been suggested as a basis for explainable AI. Such applications draw attention to the scalability of implementations. The defeasible logic $DL(\partial_{||})$ was introduced as a more scalable alternative to $DL(\partial)$, which is better known. In this paper we consider the use of (implementations of) $DL(\partial_{||})$ as a computational aid to computing conclusions in $DL(\partial)$ and other defeasible logics, rather than as an alternative to $DL(\partial)$. We identify condition…
We develop a modal logic to capture partial awareness. The logic has three building blocks: objects, properties, and concepts. Properties are unary predicates on objects; concepts are Boolean combinations of properties. We take an agent to be partially aware of a concept if she is aware of the concept without being aware of the properties that define it. The logic allows for quantification over objects and properties, so that the agent can reason about her own unawareness. We then apply the logic to contracts, which we view as syntactic objects that dictate outcomes based on the truth of formu…
Institut de Recherche en Informatique de Toulouse (I.R.I.T.)（图卢兹计算机科学研究所）；Universite Paul Sabatier（保尔·萨巴蒂埃大学）
A semantics is given to possibilistic logic, a logic that handles weighted classical logic formulae, and where weights are interpreted as lower bounds on degrees of certainty or possibility, in the sense of Zadeh's possibility theory. The proposed semantics is based on fuzzy sets of interpretations. It is tolerant to partial inconsistency. Satisfiability is extended from interpretations to fuzzy sets of interpretations, each fuzzy set representing a possibility distribution describing what is known about the state of the world. A possibilistic knowledge base is then viewed as a set of possibil…
Contextuality is a key signature of quantum non-classicality, which has been shown to play a central role in enabling quantum advantage for a wide range of information-processing and computational tasks. We study the logic of contextuality from a structural point of view, in the setting of partial Boolean algebras introduced by Kochen and Specker in their seminal work. These contrast with traditional quantum logic à la Birkhoff and von Neumann in that operations such as conjunction and disjunction are partial, only being defined in the domain where they are physically meaningful. We study how …
Resolution and superposition are common techniques which have seen widespread use with propositional and first-order logic in modern theorem provers. In these cases, resolution proof production is a key feature of such tools; however, the proofs that they produce are not necessarily as concise as possible. For propositional resolution proofs, there are a wide variety of proof compression techniques. There are fewer techniques for compressing first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on li…
We show a model construction for a system of higher-order illative combinatory logic $\mathcal{I}_ω$, thus establishing its strong consistency. We also use a variant of this construction to provide a complete embedding of first-order intuitionistic predicate logic with second-order propositional quantifiers into the system $\mathcal{I}_0$ of Barendregt, Bunder and Dekkers, which gives a partial answer to a question posed by these authors.
This paper establishes the normalisation of natural deduction or lambda calculus formulation of Intuitionistic Non Commutative Logic --- which involves both commutative and non commutative connectives. This calculus first introduced by de Groote and as opposed to the classical version by Abrusci and Ruet admits a full entropy which allow order to be relaxed into any suborder. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Regarding Intuitionistic Non Commutative Logic with full entrop…
Standard approaches to probabilistic reasoning require that one possesses an explicit model of the distribution in question. But, the empirical learning of models of probability distributions from partial observations is a problem for which efficient algorithms are generally not known. In this work we consider the use of bounded-degree fragments of the "sum-of-squares" logic as a probability logic. Prior work has shown that we can decide refutability for such fragments in polynomial-time. We propose to use such fragments to answer queries about whether a given probability distribution satisfie…
Program slicing has been mainly studied in the context of imperative languages, where it has been applied to a wide variety of software engineering tasks, like program understanding, maintenance, debugging, testing, code reuse, etc. This work introduces the first forward slicing technique for declarative multi-paradigm programs which integrate features from functional and logic programming. Basically, given a program and a slicing criterion (a function call in our setting), the computed forward slice contains those parts of the original program which are reachable from the slicing criterion. O…
Centre for Artificial Intelligence Research（人工智能研究中心）；University of KwaZulu-Natal（夸祖鲁-纳塔尔大学）；CSIR Meraka Institute（科学与工业研究理事会梅拉卡研究所）
Standard belief change assumes an underlying logic containing full classical propositional logic. However, there are good reasons for considering belief change in less expressive logics as well. In this paper we build on recent investigations by Delgrande on contraction for Horn logic. We show that the standard basic form of contraction, partial meet, is too strong in the Horn case. This result stands in contrast to Delgrande's conjecture that orderly maxichoice is the appropriate form of contraction for Horn logic. We then define a more appropriate notion of basic contraction for the Horn cas…
We prove that the category of vector bundles over a fixed smooth manifold and its corresponding category of convenient modules are models for intuitionistic differential linear logic. The exponential modality is modelled by composing the jet comonad, whose Kleisli category has linear differential operators as morphisms, with the more familiar distributional comonad, whose Kleisli category has smooth maps as morphisms. Combining the two comonads gives a new interpretation of the semantics of differential linear logic where the Kleisli morphisms are smooth local functionals, or equivalently, smo…
Wegner describes coordination as constrained interaction. We take this approach literally and define a coordination model based on interaction constraints and partial, iterative and interactive constraint satisfaction. Our model captures behaviour described in terms of synchronisation and data flow constraints, plus various modes of interaction with the outside world provided by external constraint symbols, on-the-fly constraint generation, and coordination variables. Underlying our approach is an engine performing (partial) constraint satisfaction of the sets of constraints. Our model extends…
We study the underlying mathematical properties of various partial order models of concurrency based on transition systems, Petri nets, and event structures, and show that the concurrent behaviour of these systems can be captured in a uniform way by two simple and general dualities of local behaviour. Such dualities are used to define new mu-calculi and logic games for the analysis of concurrent systems with partial order semantics. Some results of this work are: the definition of a number of mu-calculi which, in some classes of systems, induce the same identifications as some of the best know…
A number of extensions exist for Alternating-time Temporal Logic; some of these mix strategies and partial observability but, to the best of our knowledge, no work provides a unified framework for strategies, partial observability and fairness constraints. In this paper we propose ATLK^F_po, a logic mixing strategies under partial observability and epistemic properties of agents in a system with fairness constraints on states, and we provide a model checking algorithm for it.
This paper concerns a goal directed proof procedure for the propositional fragment of the adaptive logic ACLuN1. At the propositional level, it forms an algorithm for final derivability. If extended to the predicative level, it provides a criterion for final derivability. This is essential in view of the absence of a positive test. The procedure may be generalized to all flat adaptive logics.
A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of…
In this paper we propose an extension of Answer Set Programming (ASP), and in particular, of its most general logical counterpart, Quantified Equilibrium Logic (QEL), to deal with partial functions. Although the treatment of equality in QEL can be established in different ways, we first analyse the choice of decidable equality with complete functions and Herbrand models, recently proposed in the literature. We argue that this choice yields some counterintuitive effects from a logic programming and knowledge representation point of view. We then propose a variant called QELF where the set of fu…
Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model-checking problem, even for very expr…
Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics--proof systems that manipulate trees whose nodes are multisets of formulae--and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel …
We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.
Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at first-order tool support. In this paper, we precisely connect the semantics of these two logics. We define a logic whose syntax subsumes both that of a standard separation logic, and that of implicit dynamic frames as sub-syntaxes. We define a total heap semantics for our logic, and, for the separation logic subsyntax, prove it equivalent the standard partial heaps model. In order to def…
We propose a formal model of distributed computing based on register automata that captures a broad class of synchronous network algorithms. The local memory of each process is represented by a finite-state controller and a fixed number of registers, each of which can store the unique identifier of some process in the network. To underline the naturalness of our model, we show that it has the same expressive power as a certain extension of first-order logic on graphs whose nodes are equipped with a total order. Said extension lets us define new functions on the set of nodes by means of a so-ca…
Program specialization is a program transformation methodology which improves program efficiency by exploiting the information about the input data which are available at compile time. We show that current techniques for program specialization based on partial evaluation do not perform well on nondeterministic logic programs. We then consider a set of transformation rules which extend the ones used for partial evaluation, and we propose a strategy for guiding the application of these extended rules so to derive very efficient specialized programs. The efficiency improvements which sometimes ar…
I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features. Holophrasm exploits the formalism of the Metamath language and explores partial proof trees using a neural-network-augmented bandit algorithm and a sequence-to-sequence model for action enumeration. The system proves 14% of its test theorems from Metamath's set.mm module.
We discuss the syntax and semantics of relational Horn logic (RHL) and partial Horn logic (PHL). RHL is an extension of the Datalog programming language that allows introducing and equating variables in conclusions. PHL is a syntactic extension of RHL by partial functions and one of the many equivalent notions of essentially algebraic theory. Our main contribution is a new construction of free models. We associate to RHL and PHL sequents classifying morphisms, which enable us to characterize logical satisfaction using lifting properties. We then obtain free and weakly free models using the sma…
We formalise the well-known rules of partial differentiation in a version of equational logic with function variables and binding constructs. We prove the resulting theory is complete with respect to polynomial interpretations. The proof makes use of Severi's interpolation theorem that all multivariate Hermite problems are solvable. We also present a number of related results, such as decidability and equational completeness.
We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs are linear in the length of the program. We argue that in spite of the fact that Hoare-like proof systems for recursive procedures were intensively studied, no such proof system has been proposed in the literature.
