Episteme - dmlc - Logic Symbols

Extracting Logic Symbols

The dmlc walks the parse tree for the logical markup of a proposition and records all variables, their type, and some other potentially useful information. Here is the logical markup for the first step of Archimedes' second proposition in FB I along with the corresponding logical symbol table entries.

	...
	<dialog:step n='1'>
	  <dialog:given>
	    <tlg0552.tlg008:fluid_surface id='ul_abcd'>
	      <tlg0552.tlg008:center_of_earth id='o'/>
	    </tlg0552.tlg008:fluid_surface>
	    <tlg1799.tlg001:plane_surface id='ul_abcdo'>
	      <dialog:associateType ref='o' type='tlg1799.tlg001:point'/>
	    </tlg1799.tlg001:plane_surface>
	  </dialog:given>
	  <dialog:do>
	    <tlg1799.tlg001:intersection>
	      <dialog:emergent_primitives>
	        <tlg0552.tlg008:curve id='abcd'>
	          <tlg1799.tlg001:point id='a'/>
	          <tlg1799.tlg001:point id='b'/>
	          <tlg1799.tlg001:point id='c'/>
	          <tlg1799.tlg001:point id='d'/>
	        </tlg0552.tlg008:curve>
	      </dialog:emergent_primitives>
	    <tlg0552.tlg008:fluid_surface ref='ul_abcd'/>
	    <tlg1799.tlg001:plane_surface ref='ul_abcdo'/>
	    </tlg1799.tlg001:intersection>
	  </dialog:do>
	</dialog:step>	
	...
      

	

	  
name
type
	  
ul_abcd
tlg0552.tlg008:fluid_surface
	  
o
tlg0552.tlg008:center_of_earth,tlg1799.tlg001:point
	  
ul_abcdo
tlg1799.tlg001:plane_surface
	  
abcd
tlg0552.tlg008:curve
	  
a
tlg1799.tlg001:point
	  
b
tlg1799.tlg001:point
	  
c
tlg1799.tlg001:point
	  
d
tlg1799.tlg001:point
	
      

In this table, we see all the variables declared in the course of a proposition, their labels (name), and the logical types which they take on. There is also information useful for type-checking here.