The Soundness and Completeness Proof of Agent Intention in AgentSpeak

2007 ◽  
Author(s):  
Yang Bo ◽  
Qin Zheng ◽  
Yu Fan ◽  
Qin Jun
Keyword(s):  
Completeness Proof ◽  
Soundness And Completeness

scholarly journals The logic of interactive turing reduction

2007 ◽  
Vol 72 (1) ◽  
pp. 243-276 ◽  
Author(s):  
Giorgi Japaridze
Keyword(s):  
Input Output ◽  
Completeness Proof ◽  
Turing Reducibility ◽  
Soundness And Completeness ◽  
Turing Reduction

AbstractThe paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept — more precisely, the associated concept of reducibility — is a generalization of Turing reducibility from the traditional, input/output sorts of problems to computational tasks of arbitrary degrees of interactivity.

An axiomatic version of positive semilattice relevance logic

1981 ◽  
Vol 46 (2) ◽  
pp. 233-239 ◽  
Author(s):  
G. Charlwood
Keyword(s):  
Natural Deduction ◽  
Relevance Logic ◽  
Truth Conditions ◽  
Completeness Proof ◽  
Relevant Implication ◽  
Soundness And Completeness ◽  
Minimal Modification ◽  
Positive Relevance

In [8] and [9] Urquhart presented the semilattice semantics for a relevance logic with conjunction and disjunction. These semantics combined the simplest known semantics for relevant implication, with minimal modification of the truth conditions for conjunction and disjunction. A slightly different approach leads to the distinct positive relevance logic of [7] and [5]. Sound and complete axiomatic logics for the semilattice semantics were readily available, so long as disjunction was left out.The purpose of this paper is to report the remedy of this lack. In [1] the author developed work of Fine ([3], announced in [4]) and Prawitz [6] to show soundness and completeness of an axiomatic logic and two natural deduction logics, with respect to Urquhart's semantics. Thus Prawitz' positive relevance logic is equivalent to the semilattice logic, rather than the logic of [5]. We present here the axiomatic logic and show its equivalence to the semilattice semantics.In §1 the languages and logic are given, along with a few proof-theoretic remarks. In §2 the semantics are defined, and the soundness proof is sketched. In §3, the completeness proof is given.

scholarly journals Kripke Semantics for Intersection Formulas

2021 ◽  
Vol 22 (3) ◽  
pp. 1-16
Author(s):  
Andrej Dudenhefner ◽  
Paweł Urzyczyn
Keyword(s):  
Kripke Semantics ◽  
Type Assignment ◽  
Soundness And Completeness

We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.

An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until1

1992 ◽  
Vol 17 (3) ◽  
pp. 271-282
Author(s):  
Y.S. Ramakrishna ◽  
L.E. Moser ◽  
L.K. Dillon ◽  
P.M. Melliar-Smith ◽  
G. Kutty
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Time ◽  
Computer Systems ◽  
Hierarchical Abstraction ◽  
Soundness And Completeness

We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed.

scholarly journals Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽  
2019 ◽  
Vol 8 (4) ◽  
pp. 115 ◽  
Author(s):  
Joanna Golińska-Pilarek ◽  
Magdalena Welle
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Classical Propositional Logic ◽  
Tableau System ◽  
Soundness And Completeness

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.

scholarly journals On Polymorphic Sessions and Functions

2021 ◽  
Vol 43 (2) ◽  
pp. 1-55
Author(s):  
Bernardo Toninho ◽  
Nobuko Yoshida
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Linear Formulation ◽  
Session Types ◽  
Logical Foundation ◽  
Π Calculus ◽  
Soundness And Completeness ◽  
System F ◽  
Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

An algebraic study of Diodorean modal systems

1965 ◽  
Vol 30 (1) ◽  
pp. 58-64 ◽  
Author(s):  
R. A. Bull
Keyword(s):  
Discrete Time ◽  
Decision Procedure ◽  
John Locke ◽  
Original Model ◽  
Completeness Proof ◽  
Semantic Tableaux ◽  
Algebraic Treatment ◽  
Algebraic Result ◽  
Modal Systems

Attention was directed to modal systems in which ‘necessarily α’ is interpreted as ‘α. is and always will be the case’ by Prior in his John Locke Lectures of 1956. The present paper shows that S4.3, the extension of S4 withALCLpLqLCLqLp,is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 withALNLpLCLCLCpLpLpLp,is complete with respect to this interpretation when time is taken to be discrete. The method employed depends upon the application of an algebraic result of Garrett Birkhoff's to the models for these systems, in the sense of Tarski.A considerable amount of work on S4.3 and D precedes this paper. The original model with discrete time is given in Prior's [7] (p. 23, but note the correction in [8]); that taking time to be continuous yields a weaker system is pointed out by him in [9]. S4.3 and D are studied in [3] of Dummett and Lemmon, where it is shown that D includes S4.3 andCLCLCpLpLpCMLpLp.While in Oxford in 1963, Kripke proved that these were in fact sufficient for D, using semantic tableaux. A decision procedure for S4.3, using Birkhoff's result, is given in my [2]. Dummett conjectured, in a conversation, that taking time to be continuous yielded S4.3. Thus the originality of this paper lies in giving a suitable completeness proof for S4.3, and in the unified algebraic treatment of the systems. It should be emphasised that the credit for first axiomatising D belongs to Kripke.

A Modal Semantics of Negation in Logic Programming

1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani
Keyword(s):  
Modal Logic ◽  
Logic Programming ◽  
Modal Logics ◽  
Kripke Models ◽  
Logic Programs ◽  
Modal Semantics ◽  
Soundness And Completeness ◽  
Modal Completion ◽  
Well Foundedness

The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.

Modulated fibring and the collapsing problem

2002 ◽  
Vol 67 (4) ◽  
pp. 1541-1569 ◽  
Author(s):  
Cristina Sernadas ◽  
João Rasga ◽  
Walter A. Carnielli
Keyword(s):  
Mathematical Logic ◽  
Soundness And Completeness ◽  
The Given ◽  
Combining Logics

AbstractFibring is recognized as one of the main mechanisms in combining logics, with great significance in the theory and applications of mathematical logic. However, an open challenge to fibring is posed by the collapsing problem: even when no symbols are shared, certain combinations of logics simply collapse to one of them, indicating that fibring imposes unwanted interconnections between the given logics. Modulated fibring allows a finer control of the combination, solving the collapsing problem both at the semantic and deductive levels. Main properties like soundness and completeness are shown to be preserved, comparison with fibring is discussed, and some important classes of examples are analyzed with respect to the collapsing problem.

Sign in / Sign up

Export Citation Format

Share Document