A typed parallel lambda-calculus via 1-depth intermediate proofs

We introduce a Curry–Howard correspondence for a large class of intermediate logics characterized by intuitionistic proofs with non-nested applications of rules for classical disjunctive tautologies (1-depth intermediate proofs). The resulting calculus, we call it λ∥, is a strongly normalizing parallel extension of the simply typed λ-calculus. Although simple, the λ∥ reduction rules can model arbitrary process network topologies, and encode interesting parallel programs ranging from numeric computation to algorithms on graphs.

HEREDITARILY STRUCTURALLY COMPLETE POSITIVE LOGICS

Positive logics are $\{ \wedge , \vee , \to \}$-fragments of intermediate logics. It is clear that the positive fragment of $Int$ is not structurally complete. We give a description of all hereditarily structurally complete positive logics, while the question whether there is a structurally complete positive logic which is not hereditarily structurally complete, remains open.

On the Negative Disjunction Property

In the field of intermediate logics, the concept of the disjunction property (DP) plays an important part. Lloyd Humberstone has drawn my attention to an analogious principle called the Negative Disjunction Property ( NDP) which applies when the disjuncts involved are negated. The author investigates the NDP in the case of intermediate propositional logics. Key words: intermediate logic, disjunction property, negative disjunction property, Heyting algebra, Jankov

Automated Theorem Proving by Translation to Description Logic

Many Automated Theorem Proving (ATP) systems for different logics,and translators for translating different logics from one to another,have been developed and are now available.Some logics are more expressive than others, and it is easier to express problems in those logics.However, their ATP systems are relatively newer,and need more development and testing in order to solve more problems in a reasonable time.To benefit from the available tools to solve more problems in more expressive logics,different ATP systems and translators can be combined.Problems in logics more expressive than CNF can be translated directly to CNF, or indirectly by translation via intermediate logics.Description Logic (DL) sits between CNF and propositional logic.Saffron a CNF to DL translator, has been developed, which fills the gap between CNF and DL.ATP by translation to DL is now an alternative way of solving problems expressed in logics more expressive than DL,by combining necessary translators from those logics to CNF, Saffron, and a DL ATP system.