package de.tu_dresden.lat.forgettingBasedProofs

import de.tu_dresden.lat.forgettingBasedProofs.adaptors.{FameBasedForgetter, LetheBasedForgetter, OWLApiBasedJustifier}
import org.semanticweb.owlapi.apibinding.OWLManager

class LetheBasedALCHProofGenerator
  extends ForgettingBasedProofGenerator(
    LetheBasedForgetter.ALCH,
    OWLApiBasedJustifier.UsingHermiT(OWLManager.createOWLOntologyManager()),
    skipSteps = false)

class LetheBasedALCHProofGeneratorSkippingSteps
  extends ForgettingBasedProofGenerator(
    LetheBasedForgetter.ALCH,
    OWLApiBasedJustifier.UsingHermiT(OWLManager.createOWLOntologyManager()),
    skipSteps = true)

class LetheBasedKBProofGenerator
  extends ForgettingBasedProofGenerator(
    LetheBasedForgetter.ALC_ABox,
    OWLApiBasedJustifier.UsingHermiT(OWLManager.createOWLOntologyManager()),
    skipSteps = false
  )

class LetheBasedKBProofGeneratorSkippingSteps
  extends ForgettingBasedProofGenerator(
    LetheBasedForgetter.ALC_ABox,
    OWLApiBasedJustifier.UsingHermiT(OWLManager.createOWLOntologyManager()),
    skipSteps = true
  )


class FameBasedProofGenerator
  extends ForgettingBasedProofGenerator(
    new FameBasedForgetter(),
    OWLApiBasedJustifier.UsingHermiT(OWLManager.createOWLOntologyManager()),
    skipSteps = false
  )

class FameBasedProofGeneratorSkippingSteps
  extends ForgettingBasedProofGenerator(
    new FameBasedForgetter(),
    OWLApiBasedJustifier.UsingHermiT(OWLManager.createOWLOntologyManager()),
    skipSteps = true
  )