mirror of
https://github.com/RAIRLab/Spectra.git
synced 2024-11-25 10:26:34 -05:00
55 lines
2.4 KiB
Text
55 lines
2.4 KiB
Text
|
;--------------------------------------------------------------------------
|
||
|
|
; File : LCL109-2 : TPTP v2.2.0. Released v1.0.0.
|
||
|
|
; Domain : Logic Calculi (Many valued sentential)
|
||
|
|
; Problem : MV-4 depends on the Merideth system
|
||
|
|
; Version : [Ove90] axioms.
|
||
|
|
; Theorem formulation : Wajsberg algebra formulation.
|
||
|
|
; English : An axiomatisation of the many valued sentential calculus
|
||
|
|
; is {MV-1,MV-2,MV-3,MV-5} by Meredith. Wajsberg provided
|
||
|
|
; a different axiomatisation. Show that MV-4 depends on the
|
||
|
|
; Wajsberg system.
|
||
|
|
|
||
|
|
; Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||
|
|
; : [LM92] Lusk & McCune (1992), Experiments with ROO, a Parallel
|
||
|
|
; : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit
|
||
|
|
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||
|
|
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||
|
|
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in
|
||
|
|
; Source : [Ove90]
|
||
|
|
; Names : CADE-11 Competition Eq-5 [Ove90]
|
||
|
|
; : Luka-5 [LM92]
|
||
|
|
; : MV4 [LW92]
|
||
|
|
; : THEOREM EQ-5 [LM93]
|
||
|
|
; : PROBLEM 5 [Zha93]
|
||
|
|
|
||
|
|
; Status : unsatisfiable
|
||
|
|
; Rating : 0.56 v2.2.0, 0.71 v2.1.0, 1.00 v2.0.0
|
||
|
|
; Syntax : Number of clauses : 5 ( 0 non-Horn; 5 unit; 1 RR)
|
||
|
|
; Number of literals : 5 ( 5 equality)
|
||
|
|
; Maximal clause size : 1 ( 1 average)
|
||
|
|
; Number of predicates : 1 ( 0 propositional; 2-2 arity)
|
||
|
|
; Number of functors : 5 ( 3 constant; 0-2 arity)
|
||
|
|
; Number of variables : 8 ( 0 singleton)
|
||
|
|
; Maximal term depth : 4 ( 2 average)
|
||
|
|
|
||
|
|
; Comments :
|
||
|
|
; : tptp2X -f kif -t rm_equality:rstfp LCL109-2.p
|
||
|
|
; ; 'true' renamed to 'true0' - MES
|
||
|
|
;--------------------------------------------------------------------------
|
||
|
|
; wajsberg_1, axiom.
|
||
|
|
(or (= (implies true0 ?A) ?A))
|
||
|
|
|
||
|
|
; wajsberg_2, axiom.
|
||
|
|
(or (= (implies (implies ?A ?B) (implies (implies ?B ?C) (implies ?A ?C))) true0))
|
||
|
|
|
||
|
|
; wajsberg_3, axiom.
|
||
|
|
(or (= (implies (implies ?A ?B) ?B) (implies (implies ?B ?A) ?A)))
|
||
|
|
|
||
|
|
; wajsberg_4, axiom.
|
||
|
|
(or (= (implies (implies (not ?A) (not ?B)) (implies ?B ?A)) true0))
|
||
|
|
|
||
|
|
; prove_wajsberg_mv_4, conjecture.
|
||
|
|
(or (/= (implies (implies (implies a b) (implies b a)) (implies b a)) true0))
|
||
|
|
|
||
|
|
;--------------------------------------------------------------------------
|