• Home
• About Coq
• Get Coq
• Documentation
• Community

Library TestErgo

Library Generators

• Pigeon hole formulas
• Pigeon hole formulas (revisited)
• De Bruijn formula
• De Bruijn formula (in 2-SAT CNF)
• Associativity of equivalences
• Franzen formulas
• Schwichtenberg formulas
• Two formulas to test the sharing of subformulas

Library GeneratorsNG

• Pigeon hole formulas
• De Bruijn formula

Library GeneratorsEq

Library EinsteinEasy

Library EinsteinEasy2

Library Demo

Library AltDemo

Library Ergo.Use

Library Ergo.Uf

Library Ergo.Theory

• Theory
• TheorySpecs
• Example

Library Ergo.TheoryArith

Library Ergo.Term

• Different kinds of arithmetic that we handle
• Reification of types
• Terms

Library Ergo.TermUtils

Library Ergo.TacticLazy

• The functor Adequation
• The functor LoadTactic

Library Ergo.SemLazy

Library Ergo.Semantics

• The module type SEM_INTERFACE
• The functor SEMANTICS
• The functor SemFacts
  • Model properties

Library Ergo.Sat

• The main functor SAT
  • Definition of the proof derivation system
  • Correctness of the inference rules
  • A naive strategy for proof search
  • Soundness and completeness proofs for the proof search
  • The main entry point to the SAT-solver

Library Ergo.SatCaml

• The functor SATSTRATEGY
  • Functions computing the BCP
  • The main proof_search function
  • The main entry point to the SAT-solver

Library Ergo.Rational

Library Ergo.ModelsRingExt

• soit la règle utilisée dans u <->p w est de R, auquel cas
• soit la règle utilisée est ~, auquel cas...

Library Ergo.LLazy

• Preliminary results on list comparison
• A module type LITERALBASE from which
• The module type LITERAL
• The module RAW
  • Comparison on literals
• The module LLAZY
  • atom as an OrderedType

Library Ergo.Literal

• The module type LITERAL

Library Ergo.Lexico

Library Ergo.Index

• The module INDEX

Library Ergo.FoldProps

Library Ergo.Ergo

Library Ergo.Env

Library Ergo.EnvLazy

Library Ergo.Dpll

• The module type DPLL

Library Ergo.DoubleNegUtils

Library Ergo.DistrNeg

Library Ergo.Diff

Library Ergo.DiagProd

Library Ergo.CPolynoms

Library Ergo.Cnf

• The module type CNF

Library Ergo.CNFLazy

• The module CNFRAW
• The module CNFLAZY

Library Ergo.CNFLazyN

• The module CNFLAZYN

Library Ergo.CNFLazyCommon

• The module type CNFLAZY_INTERFACE
• The module CNFLAZYCOMMON

Library Ergo.CCX

Library Ergo.AltErgo

Library Ergo.AllInstances

Library Ergo.Adequation

• webmaster
• xhtml valid
• CSS valid