Displaying similar documents to “Quantum logics with classically determined states”

The Derivations of Temporal Logic Formulas

Mariusz Giero (2012)

Formalized Mathematics

Similarity:

This is a preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [12]. We introduce n-ary connectives and prove their properties. We derive temporal logic formulas.

Program Algebra over an Algebra

Grzegorz Bancerek (2012)

Formalized Mathematics

Similarity:

We introduce an algebra with free variables, an algebra with undefined values, a program algebra over a term algebra, an algebra with integers, and an algebra with arrays. Program algebra is defined as universal algebra with assignments. Programs depend on the set of generators with supporting variables and supporting terms which determine the value of free variables in the next state. The execution of a program is changing state according to successor function using supporting terms. ...

The Properties of Sets of Temporal Logic Subformulas

Mariusz Giero (2012)

Formalized Mathematics

Similarity:

This is a second preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [17]. We introduce two modified definitions of a subformula. In the former one we treat until-formula as indivisible. In the latter one, we extend the set of subformulas of until-formulas by a special disjunctive formula. This is needed to construct a temporal model. We also...

Monotone sequent calculus and resolution

Marta Bílková (2001)

Commentationes Mathematicae Universitatis Carolinae

Similarity:

We study relations between propositional Monotone Sequent Calculus (MLK --- also known as Geometric Logic) and Resolution with respect to the complexity of proofs, namely to the concept of the polynomial simulation of proofs. We consider Resolution on sets of monochromatic clauses. We prove that there exists a polynomial simulation of proofs in MLK by intuitionistic proofs. We show a polynomial simulation between proofs from axioms in MLK and corresponding proofs of contradiction (refutations)...