scientific article; zbMATH DE number 1045389

MaRDI QIDQ4347145zbMATH OpenFDO

Authors Alex Hendriks

Publication date 7 August 1997

zbMATH Keywords

derivabilityexact modelsfinite fragments of propositional logicsfinite Lindenbaum algebraintuitionistic logicmodal logicmodel checkingvalidity of formulas

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Model theory of finite structures (03C13)

Review text

The main topic of this thesis is the representation of fragments of intuitionistic and modal propositional logic by (usually finite) structures, called exact models. One of the reasons for the interest in properties of fragments with such a finite representation is the possibility of designing computer programs to decide derivability within the fragment. In general, this kind of program, based on checking the validity of formulas in a model, is much more efficient than traditional theorem proving. This efficiency of `model checking versus theorem proving' has in recent years attracted the attention of researchers in artificial intelligence and knowledge representation. For the benefits of model checking we have to pay a price. Theorem provers are `general purpose' tools, accepting any formula in the language of the logic (obviously with certain practical limitations). However, finite representations such as exact models exist only when we cut down the expressive power of the language. In this thesis we focus our attention on finite fragments of propositional logics, laguages with restrictions on the use of atomic subformulas and connectives, that have a finite Lindenbaum algebra or diagram as we prefer to call it here. The structure of these finite diagrams can be calculated and studied using efficient computer programs based on model checking. Knowledge of the structure of diagrams can be used in constructing new finite complete models.

Recommendations

• Computations in fragments of intuitionistic propositional logic
• scientific article; zbMATH DE number 823603
• Intuitionistic implication without disjunction
• Effective Finite-Valued Approximations of General Propositional Logics

Cited in

(16)

• The many faces of interpolation
• Partial-predicate logic in computer science
• Computations in fragments of intuitionistic propositional logic
• Doing logic by computer: Interpolation in fragments of intuitionistic propositional logic
• Algebras defined from ordered sets and the varieties they generate
• scientific article; zbMATH DE number 5841868 (Why is no real title available?)
• Duality and universal models for the meet-implication fragment of IPC
• DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV
• Brodskio kodavimo metodas teiginių logikai;Brodsky’s coding method for propositional logic
• Propositional computability logic I
• Propositional computability logic II
• Towards logical operations research -- propositional case
• Toggling operators in computability logic
• Notes on my scientific life
• Intermediate logics and factors of the Medvedev lattice
• Free equivalential algebras

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4347145)