Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: parallel reasoning

Sortuj według:

Ogranicz wyniki do:

Multi-Agent Dialogues and Dialogue Sequents for Proof Search and Scheduling in Intuitionistic Logic and the Modal Logic S4

100%

Sticht M.

tom Vol. 161, nr 1/2

191--218

Dialogical games as introduced by Lorenzen and Lorenz describe a reasoning technique for intuitionistic and classical predicate logic: two players (proponent and opponent) argue about the validity of a given formula according to predefined rules. If the proponent has a winning strategy then the formula is proven to be valid. The underlying game rules can be modified to have an impact on proof search strategies and increase the efficiency of such a searching process. In this paper, a multi-agent version of dialogical logic is introduced that corresponds more to multiconclusion sequent calculi for propositional intuitionistic logic rather than single-conclusion ones which are more related to two-player dialogues. We also consider an extension for the normal modal logic S4. The rules lead us to a normalization of a proof, let us focus on the proponents' relevant decisions, and therefore give explicit directives that increase compactness of the proofsearching process. This allows us to perform parts of the proof in a parallel way. We prove soundness and completeness of these multi-agent systems.

Experimental analysis of some computation rules in a simple parallel reasoning system for the ALC description logic

100%

Meissner A.

tom Vol. 21, no 1

83-95

A computation rule determines the order of selecting premises during an inference process. In this paper we empirically analyse three particular computation rules in a tableau-based, parallel reasoning system for the ALC description logic, which is built in the relational programming model in the Oz language. The system is constructed in the lean deduction style, namely, it has the form of a small program containing only basic mechanisms, which assure soundness and completeness of reasoning. In consequence, the system can act as a convenient test-bed for comparing various inference algorithms and their elements. We take advantage of this property and evaluate the studied methods of selecting premises with regard to their efficiency and speedup, which can be obtained by parallel processing.