Packages

p

gapt

provers

package provers

Content Hierarchy
Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Package Members

  1. package congruence
  2. package eprover
  3. package escargot
  4. package iprover
  5. package leancop
  6. package maxsat
  7. package metis
  8. package prover9
  9. package sat
  10. package simp
  11. package slakje
  12. package smtlib
  13. package spass
  14. package vampire
  15. package verit
  16. package viper

Type Members

  1. trait IncrementalProver extends Prover

    A prover that determines validity via an incremental proof session.

  2. trait OneShotProver extends Prover

    A prover that interprets Sessions as stack operations.

  3. trait Prover extends AnyRef

    A prover that is able to refute HOL sequents/formulas (or subsets of HOL, like propositional logic).

    A prover that is able to refute HOL sequents/formulas (or subsets of HOL, like propositional logic).

    TODO: exceptions to indicate that a formula is not supported (e.g. for propositional provers).

    Implementors may want to override isValid(seq) to avoid parsing proofs.

  4. trait ResolutionProver extends OneShotProver

Value Members

  1. object Session

    Implementation of proof sessions via the cats free monad.

    Implementation of proof sessions via the cats free monad. See http://typelevel.org/cats/datatypes/freemonad.html.

  2. object extractIntroducedDefinitions
  3. object groundFreeVariables
  4. object mangleName
  5. object renameConstantsToFi

Ungrouped