(=>
(and
(instance ?TRANS FinancialTransaction)
(attribute ?TRANS BusinessToConsumer))
(exists (?ACCT1 ?ACCT2 ?USER1 ?USER2 ?SITE)
(and
(instance ?ACCT1 UserAccount)
(instance ?ACCT2 UserAccount)
(instance ?USER1 AutonomousAgent)
(instance ?USER2 AutonomousAgent)
(instance ?SITE WebSite)
(agent ?TRANS ?USER1)
(destination ?TRANS ?USER2)
(instrument ?TRANS ?SITE)
(hasAccount ?USER1 ?ACCT1)
(hasAccount ?USER2 ?ACCT2)
(accountAtSite ?ACCT1 ?SITE)
(accountAtSite ?ACCT2 ?SITE)
(attribute ?ACCT1 BusinessAccount)
(attribute ?ACCT2 ConsumerAccount)))) |
UXExperimentalTerms.kif 1760-1779 |
If X is an instance of financial transaction and business to consumer transaction is an attribute of X, then All of the following hold: (1) there exist Y, Z,, , W,, , V (2) U such that Y is an instance of user account (3) Z is an instance of user account (4) W is an instance of agent (5) V is an instance of agent (6) U is an instance of web site (7) W is an agent of X (8) X ends up at V (9) U is an instrument for X (10) W has account Y (11) V has account Z (12) Y is an account at U (13) Z is an account at U (14) business account is an attribute of Y (15) consumer account is an attribute of Z |
BusinessToConsumer