Package: prover9 (0.0.200911a-2.1 and others)

[ Source: ladr  ]

bevisudførelse for teoremer og oprettelsesmodel for modmodel

Denne pakke tilbyder Prover9's bevissystem for resolutioner/paramodulation og Mace4's opretter af modbeviser.

Prover9 foretager automatiserede bevisudførelser for teoremer i prædikatlogik og ligningslogik. Det er efterfølgeren for Otter- bevissystemet for teoremer. Prover9 bruger de samme slutningsteknikker for ordnede resolutioner og paramodulering med udvælgelse af literaler.

Programmet Mace4 søger efter finitte strukturer, der tilfredsstiller prædikatlogik og ligningslogik, den samme slags udtryk som Prover9 accepterer. Hvis påstanden en afvisning af en antagelse, så vil alle strukturer som Mace4 finder, være modeksempler på antagelsen.

Mace4 kan være et værdifuldt tillæg til Prover9, der kigger efter modeksempler før (eller på samme tid som) brug af Prover9 til at søge efter et bevis. Programmet kan også bruges til at hjælpe med at fejlsøge inddata-klausuler og formler for Prover9.

Other Packages Related to prover9

• dep: libc6 (>= 2.17)

  GNU C-bibliotek: Delte biblioteker
  also a virtual package provided by libc6-udeb

• dep: libladr4 (>= 0.0.200911a-1)

  LADR-deduktionsbiblioteket

• sug: ladr4-apps (= 0.0.200911a-2.1+b2)

  LADR-deduktionsbiblioteket, diverse programmer

• sug: prover9-doc (<< 0.0.200902b)

  dokumentation for Prover9 og associerede programmer

  sug: prover9-doc (>> 0.0.200902a)

Download prover9

Download for all available architectures

Architecture	Version	Package Size	Installed Size	Files
arm64	0.0.200911a-2.1+b2	90.6 kB	297.0 kB	[list of files]