Displaying similar documents to “A decomposability criterion for elementary theories.”

Computational logics and the philosophy of language: the problem of lexical meaning in formal semantics.

Marcello Frixione (1996)

Mathware and Soft Computing


This paper deals with the possible contributions that logical researches carried on in the field of artificial intelligence (AI) could give to formal theories of meaning developed by logically oriented philosophers of language within the tradition of analytic philosophy. In particular, I will take into account a topic which is problematic in many respects for traditional logical accounts of meaning, i.e., the problem of lexical semantics. My thesis is that AI logics could give useful...

Cocktail: a tool for deriving correct programs.

Michael Franssen, Harrie De Swart (2004)



Cocktail is a tool for deriving correct programs from their specifications. The present version is powerful enough for educational purposes. The tool yields support for many sorted first order predicate logic, formulated in a pure type system with parametric constants (CPTS), as the specification language, a simple While-language, a Hoare logic represented in the same CPTS for deriving programs from their specifications and a simple tableau based automated theorem prover for verifying...

On some properties of grounding nonuniform sets of modal conjunctions

Radoslaw Katarzyniak (2006)

International Journal of Applied Mathematics and Computer Science


A language grounding problem is considered for nonuniform sets of modal conjunctions consisting of conjunctions extended with more than one modal operator of knowledge, belief or possibility. The grounding is considered in the context of semiotic triangles built from language symbols, communicative cognitive agents and external objects. The communicative cognitive agents are assumed to be able to observe external worlds and store the results of observations in internal knowledge bases....

A system for deduction-based formal verification of workflow-oriented software models

Radosław Klimek (2014)

International Journal of Applied Mathematics and Computer Science


The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model's behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process...

Area-oriented technology mapping for LUT-based logic blocks

Marcin Kubica, Dariusz Kania (2017)

International Journal of Applied Mathematics and Computer Science


One of the main aspects of logic synthesis dedicated to FPGA is the problem of technology mapping, which is directly associated with the logic decomposition technique. This paper focuses on using configurable properties of CLBs in the process of logic decomposition and technology mapping. A novel theory and a set of efficient techniques for logic decomposition based on a BDD are proposed. The paper shows that logic optimization can be efficiently carried out by using multiple decomposition....

Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument

Christoph Benzmüller, David Fuenmayor (2020)

Bulletin of the Section of Logic


Three variants of Kurt Gödel's ontological argument, proposed by Dana Scott, C. Anthony Anderson and Melvin Fitting, are encoded and rigorously assessed on the computer. In contrast to Scott's version of Gödel's argument the two variants contributed by Anderson and Fitting avoid modal collapse. Although they appear quite different on a cursory reading they are in fact closely related. This has been revealed in the computer-supported formal analysis presented in this article. Key to our...