Contents

• Propositionnal connective.
  • Conjunction.
  • Disjunction.
  • Propositional constants and negation.
  • Existential quantifiers.
  • Equality.
  • Some tautologies.
  • Classical logic.
  • Definite description.
  • Contraposition.
  • De Morgan Laws.
  
  
• Usual definitions on binary relations.
• Properties of basic operations and predicates on the booleans.
  • Basic definitions.
  • The introduction rules for I B.
  • Elimination rules for I B.
  • Left rules for I B.
  • Boolean equality.
  
  
• Definition of functions on booleans.
  • if ... then ... else ...
  • Boolean functions.
  
  
• Basic definitions.
  • Introduction rules for I N.
  • Elimination rules for I N.
  • left rules for = on I N
  
  
• Properties of basic operations and predicates on the product.
  • Basic definitions
  • The introduction rule for ×
  • The elimination rules for ×
  
  
• Projections
  • Definitions
  • Very basic facts
  
  
• Lexicographic ordering
• Basic definitions
• Matching
• Basic definitions and properties
  • Definitions and axioms
  • Rules on lists
  • Decidability of equality
  
  
• Defining functions by induction on lists
  • Definition
  • Application : operations on lists
  • Head and tail of a list as partial functions
  • Quantifiers bounded on lists.
  • Membership in a list
  
  
• Basic definitions
• Compatible fonctions

Basic PhoX Library Christophe Raffalli, Paul Rozière Université de Savoie, université Paris VII

Warning: This library is always loaded !