Honours-Project/complete_process.py at main · bravesirrobin358/Honours-Project · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
from utils.extract_statement import extract_section, extract_statements, read_contact
import premise_to_proposition
import string
from logics.utils.solvers.natural_deduction import classical_natural_deduction_solver
from logics.utils.parsers import classical_parser
from logics.instances.propositional.many_valued_semantics import ST_mvl_semantics as ST
import json
from logics.instances.propositional.languages import classical_language
import logics
import sys

file = "shorter.pdf" if not sys.argv[1:] else sys.argv[1]
if file.endswith(".txt"):
    with open(file) as f:
        section_text = f.read()
else:
    text = read_contact(file)
    section_text = extract_section(text)
statements = extract_statements(section_text)
print("Extracted Statements:")
for s in statements:
    print(s)

LLMProcessingPremise = premise_to_proposition.LLMProcessingPremise(model_name="llama3.1")
result = LLMProcessingPremise.process_clause(' '.join(statements), use_llm=True)
formula, variable_map = result["formula"], result["variable_map"]
rewritten_initial_conditions = formula.replace("\n"," / ").replace(" / ",", ",formula.count(" / ")-1).replace("->","→").translate(str.maketrans("⋀⋁¬","∧∨~"))

print("formula: ", rewritten_initial_conditions)
print("mapping: ")
print(json.dumps(variable_map, indent=2))


logics.instances.predicate.languages.metavariables = list(variable_map.keys())
logics.instances.propositional.languages.metavariables = list(variable_map.keys())
parsed = classical_parser.parse(rewritten_initial_conditions)
is_valid = ST.is_valid(parsed)
if not is_valid:
    print(rewritten_initial_conditions, " is not a valid inference")
    exit(1)
derivation = classical_natural_deduction_solver.solve(parsed)

# original solution
derivation.print_derivation(classical_parser)

# Find unused premise lines of the original solution
args_used = set([x for sublist in [i.on_steps for i in list(derivation)] for x in sublist])
prem_size = len(derivation)-1
unused_args = set(range(prem_size)) - args_used
unused_formulas = [derivation[i].content for i in unused_args]

print("Propositional map:\n",variable_map)


print("\nSimplified version:")

# Find and all instances of the unused formulas and remove them. Also remove any premises that consist entirely of unused formulas.
for i in unused_formulas:
    for prem in range(len(parsed.premises)):
        red = parsed.premises[prem].schematic_reduction(classical_language,parsed.premises[prem],i)
        parsed = parsed.substitute(parsed.premises[prem],red)

    parsed.premises = [p for p in parsed.premises if i != p]

#Solve again using the simplified premises
derivation = classical_natural_deduction_solver.solve(parsed)

derivation.print_derivation(classical_parser)