Handbook of Automated Reasoning

Chapter 22

Connections in Nonclassical Logics

Arild Waaler    University of Oslo, Norway

Contents

1 2Introduction   1489

2 Prelude: Connections in classical first–order logic   1491

2.1 Introduction: a sequent calculus perspective on classical matrices   1491

2.2 Language and models   1496

2.3 Free variable LK   1497

2.4 Free variable tableaux   1502

2.5 Matrices   1503

2.6 Permutation   1508

2.7 Soundness   1510

2.8 Model existence and completeness   1513

2.9 From calculus to search procedure   1514

3 Labelled systems   1516

3.1 Introduction   1516

3.2 Syntax of labels   1521

3.3 Unification   1523

3.4 Unification by constraints   1527

4 Propositional intuitionistic logic   1528

4.1 Free variable systems   1528

4.2 A ground single step system ...