search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
56 stars 18 forks source link

add consistency checkers to TPTP #1924

Closed tillmo closed 3 years ago

tillmo commented 4 years ago

currently, TPTP contains no consistency checkers. Add those consistency checkers that are available for SoftFOL. It should be relatively straightforward to adapt them for TPTP.

tillmo commented 4 years ago

Once this has been solved, the following should work:

hets-server -I
> use test.tptp
> dg basic test.tptp
> cons-checker eprover
> check-consistency
mcodescu commented 3 years ago

I've started something on branch https://github.com/spechub/Hets/tree/1924_tptp_cons_checkers

If I select darwin for consistency checking and pick the path via SoftFOL, I get an error hets: user error (Logic SoftFOL expected, but TPTP found). Is this normal? I guess we want to remove the cons checkers via SoftFOL anyways.

Also, when picking the path via TPTP, I can check that the theory is consistent, but a model cannot be reconstructed. I guess extractModelshould be implemented for CASL2TPTP_FOF.

tillmo commented 3 years ago

good that you start working on this one!

Indeed, comorphism paths that do not lead to the prover's logic should not be selectable.

Yes, extractModel should be implemented. But even without that, you should get the model in the prover's syntax.

mcodescu commented 3 years ago

Without any change, I get only

consistent, but could not reconstruct a model
extractModel not implemented for comorphism CASL2TPTP_FOF
Satisfiable
Darwin 1.4.5

Parsing /tmp/./findModel_S1804289383846930886.tptp ...
Calling /usr/bin/eprover for clausification ...

Horn problem: ignoring negative assert candidates.

Proving  ...

SZS status Satisfiable for /tmp/./findModel_S1804289383846930886.tptp

Statistics:
Close                                   :        0
Assert                                  :        8
Split                                   :        0
Resolve                                 :        0
Subsume                                 :        4
Compact                                 :        0
Productivity Filtered                   :        0
Assert Candidates                       :       10
Split Candidates                        :        0
Jumps                                   :        0
Debug                                   :        0
Global Debug                            :        0
Global Debug2                           :        0
Maximum Context Size                    :        8
Incomplete Branches                     :        0
Restarts                                :        0
Bound                                   :        2
Lemmas                                  :        0

CPU  Time (s)                           :      0.0
Memory    (MB)                          :        3

I'll just implement extractModel

mcodescu commented 3 years ago

None of the proof trees generated by the consistency checkers gives me something that can be parsed into a model:

pt:Satisfiable
Darwin 1.4.5

Parsing /tmp/./findModel_S1804289383846930886.tptp ...
Calling /usr/bin/eprover for clausification ...

Horn problem: ignoring negative assert candidates.

Proving  ...

SZS status Satisfiable for /tmp/./findModel_S1804289383846930886.tptp

Statistics:
Close                                   :        0
Assert                                  :        8
Split                                   :        0
Resolve                                 :        0
Subsume                                 :        4
Compact                                 :        0
Productivity Filtered                   :        0
Assert Candidates                       :       10
Split Candidates                        :        0
Jumps                                   :        0
Debug                                   :        0
Global Debug                            :        0
Global Debug2                           :        0
Maximum Context Size                    :        8
Incomplete Branches                     :        0
Restarts                                :        0
Bound                                   :        2
Lemmas                                  :        0

CPU  Time (s)                           :      0.0
Memory    (MB)                          :        3
==================================================
pt:
% SZS status Satisfiable
% SZS output start Model
sort_S(sK0).
sort_S(op_c).
sort_S(op_d).
sort_S(op_e).
% SZS output end Model
% Processing file: /tmp/./findModel_S16816927771714636915.tptp.prelude.tme.
% Processing file: /tmp/./findModel_S16816927771714636915.tptp.
% Processing file: /tmp/./findModel_S16816927771714636915.tptp.run.tme.
% *** RESULT: Fixedpoint,    0.000s.
% Model number:               1.
% Time:                  0.000s.
% Time in last model:    0.000s.
% Disjunction nodes:          0.
% Level cuts:                 0.
% Tableau depth:              0.
% Proof depth:                1.
% Closed branches:            0.
% Stopped branches:           0.
% Evaluation rounds:          1.
% Max weight resets:          0.
% Latest max weight:          3.
===============================================================
pt:Satisfiable
# Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S0Y
# and selection function SelectMaxLComplexAvoidPosPred.
#
# Presaturation interreduction done

# No proof found!
# SZS status Satisfiable
==========================================================
pt:Satisfiable

 No.of.Axioms: 7

 Length.of.Defs: 0

 Contains.Choice.Funs: false
.

% SZS status Satisfiable for /tmp/./findModel_S7198853861649760492.tptp : (rf:0,axioms:7,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:1,atp_calls_frequency:10,ordering:none,proof_output:0,protocol_output:false,clause_count:43,loop_count:8,foatp_calls:2,translation:fof_full)

I wonder why darwin does give an output that can be reconstructed into a model for the same theory, checked for consistency via CASL2SoftFOL:

logic CASL.PrenexAlg=

sorts S
op c : S
op d : S
op e : S
op e1 : S
op e2 : S
op e3 : S

forall X : S . X = e1 \/ X = e2 \/ X = e3 %(interpretation_domain)%

. not e1 = e2 /\ not e1 = e3 /\ not e2 = e3
                                %(interpretation_domain_distinct)%

. c = e1 /\ d = e2 /\ e = e3 %(interpretation_terms)%

However, krhyper, leo and eprover don't give a model in prover syntax via CASL2SoftFOL either.

tillmo commented 3 years ago

I think you need to call the provers with the correct options, and maybe they are set differently for SoftFOL.

mcodescu commented 3 years ago

I went through the options. Darwin indeed produces a model and for krhyper I have increased the verbosity to get a model too. Right now they are in prover syntax. For leo and eprover there seem to be no flags for producing the model.

I suggest we live with models in prover syntax for now and if we really want to have extractModel we open a new ticket.

mcodescu commented 3 years ago

Fixed by https://github.com/spechub/Hets/pull/1971