Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Term-modal logic and quantifier-free dynamic assignment logic
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2000 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

In this dissertation, we present two new sorts of computer sciencelogics.

Many powerful logics exist today for reasoning about multi-agentsystems, but in most of these it is hard to reason about an infiniteor indeterminate number of agents. Also the naming schemes used inthe logics often lack expressiveness to name agents in an intuitiveway.

To obtain a more expressive language for multi-agent reasoning and abetter naming scheme for agents, we introduce in the first part of thedissertation a family of logics called term-modal logics. A mainfeature of our logics is the use of modal operators indexed by theterms of the logics. Thus, one can quantify over variables occurringin modal operators. In term-modal logics agents can be represented byterms, and knowledge of agents is expressed with formulas within thescope of modal operators.

This gives us a flexible and uniform language for reasoning about theagents themselves and their knowledge. We give examples of theexpressiveness of the languages and provide sequent-style andtableau-based proof systems for the logics. Furthermore, we giveproofs of soundness and completeness with respect to the possibleworld semantics.

In the second part of the dissertation, we treat another problem inreasoning about multi-agent systems, namely the problem of informationupdating. We develop a dynamic logic of assignments with a scopingoperator instead of quantifiers. Function, relation symbols and logicvariables are all rigidly interpreted in our semantics, while programvariables are non-rigid. The scoping operator is used to distinguishbetween the value of a program variable before and after the executionof a program.

We provide a tableau proof system for the logic. First, the system isproved complete without the star operator, and then with the staroperator using an omega rule. The full logic is shown to beundecidable, while some interesting fragments are decidable.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2000. , p. x, 130
Series
Uppsala theses in computing science, ISSN 0283-359X ; 34
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:uu:diva-823ISBN: 91-506-1443-6 (print)OAI: oai:DiVA.org:uu-823DiVA, id: diva2:170775
Public defence
2001-01-12, Room 1311, building 1, Polacksbacken, Computing Science Department, Information Technology, Uppsala University, Uppsala, 13:15
Available from: 2000-12-22 Created: 2000-12-22 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(666 kB)905 downloads
File information
File name FULLTEXT01.pdfFile size 666 kBChecksum MD5
e4344773c06a04bc84aafd34425f443088cd93e74bc753730e9fe841f9a1e5d848247ca7
Type fulltextMimetype application/pdf

By organisation
Division of Computing ScienceComputing Science
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 905 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 970 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf