TPTP Problem File: SWV431^1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWV431^1 : TPTP v7.1.0. Released v3.6.0.
% Domain : Software Verification (Security)
% Problem : ICL^=> logic mapping to modal logic implies 'speaking_for'
% Version : [Ben08] axioms.
% English :
% Refs : [GA08] Garg & Abadi (2008), A Modal Deconstruction of Access
% : [Ben08] Benzmueller (2008), Automating Access Control Logics i
% : [BP09] Benzmueller & Paulson (2009), Exploring Properties of
% Source : [Ben08]
% Names :
% Status : CounterSatisfiable
% Rating : 0.33 v6.2.0, 0.00 v4.0.0, 1.00 v3.7.0
% Syntax : Number of formulae : 60 ( 0 unit; 34 type; 25 defn)
% Number of atoms : 144 ( 25 equality; 53 variable)
% Maximal formula depth : 9 ( 5 average)
% Number of connectives : 71 ( 3 ~; 1 |; 2 &; 64 @)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% ( 0 ~|; 0 ~&)
% Number of type conns : 132 ( 132 >; 0 *; 0 +; 0 <<)
% Number of symbols : 39 ( 34 :; 0 =)
% Number of variables : 49 ( 2 sgn; 4 !; 4 ?; 41 ^)
% ( 49 :; 0 !>; 0 ?*)
% ( 0 @-; 0 @+)
% SPC : TH0_CSA_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
%----Include axioms of multi modal logic
include('Axioms/LCL008^0.ax').
%----Include axioms of ICL logic
include('Axioms/SWV008^0.ax').
%----Include axioms of ICL^=> logic
include('Axioms/SWV008^2.ax').
%------------------------------------------------------------------------------
%----We introduce an arbitrary principal a
thf(a,type,(
a: $i > $o )).
thf(b,type,(
b: $i > $o )).
% We introduce an arbitrary atom s
thf(s,type,(
s: $i > $o )).
%----Can we prove 'speaking_for'?
thf(speaking_for,conjecture,
( iclval @ ( icl_impl @ ( icl_impl_princ @ ( icl_princ @ a ) @ ( icl_princ @ b ) ) @ ( icl_impl @ ( icl_says @ ( icl_princ @ a ) @ ( icl_atom @ s ) ) @ ( icl_says @ ( icl_princ @ b ) @ ( icl_atom @ s ) ) ) ) )).
%------------------------------------------------------------------------------